Metamath Proof Explorer


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 ( 𝑋𝐴 → [ 𝑋 ] ( 𝐴 × 𝐴 ) = 𝐴 )