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 X A X A × A = A

Proof

Step Hyp Ref Expression
1 vex x V
2 elecg x V X A x X A × A X A × A x
3 1 2 mpan X A x X A × A X A × A x
4 brxp X A × A x X A x A
5 4 baib X A X A × A x x A
6 3 5 bitrd X A x X A × A x A
7 6 eqrdv X A X A × A = A