Theorem ecxpid

Description: The equivalence class of a cartesian product is the whole set. (Contributed by Thierry Arnoux, 15-Jan-2024)

	Ref	Expression
Assertion	ecxpid	⊢ ( 𝑋 ∈ 𝐴 → [ 𝑋 ] ( 𝐴 × 𝐴 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑥 ∈ V
2		elecg	⊢ ( ( 𝑥 ∈ V ∧ 𝑋 ∈ 𝐴 ) → ( 𝑥 ∈ [ 𝑋 ] ( 𝐴 × 𝐴 ) ↔ 𝑋 ( 𝐴 × 𝐴 ) 𝑥 ) )
3	1 2	mpan	⊢ ( 𝑋 ∈ 𝐴 → ( 𝑥 ∈ [ 𝑋 ] ( 𝐴 × 𝐴 ) ↔ 𝑋 ( 𝐴 × 𝐴 ) 𝑥 ) )
4		brxp	⊢ ( 𝑋 ( 𝐴 × 𝐴 ) 𝑥 ↔ ( 𝑋 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) )
5	4	baib	⊢ ( 𝑋 ∈ 𝐴 → ( 𝑋 ( 𝐴 × 𝐴 ) 𝑥 ↔ 𝑥 ∈ 𝐴 ) )
6	3 5	bitrd	⊢ ( 𝑋 ∈ 𝐴 → ( 𝑥 ∈ [ 𝑋 ] ( 𝐴 × 𝐴 ) ↔ 𝑥 ∈ 𝐴 ) )
7	6	eqrdv	⊢ ( 𝑋 ∈ 𝐴 → [ 𝑋 ] ( 𝐴 × 𝐴 ) = 𝐴 )