Metamath Proof Explorer


Theorem xpeq1

Description: Equality theorem for Cartesian product. (Contributed by NM, 4-Jul-1994)

Ref Expression
Assertion xpeq1
|- ( A = B -> ( A X. C ) = ( B X. C ) )

Proof

Step Hyp Ref Expression
1 eleq2
 |-  ( A = B -> ( x e. A <-> x e. B ) )
2 1 anbi1d
 |-  ( A = B -> ( ( x e. A /\ y e. C ) <-> ( x e. B /\ y e. C ) ) )
3 2 opabbidv
 |-  ( A = B -> { <. x , y >. | ( x e. A /\ y e. C ) } = { <. x , y >. | ( x e. B /\ y e. C ) } )
4 df-xp
 |-  ( A X. C ) = { <. x , y >. | ( x e. A /\ y e. C ) }
5 df-xp
 |-  ( B X. C ) = { <. x , y >. | ( x e. B /\ y e. C ) }
6 3 4 5 3eqtr4g
 |-  ( A = B -> ( A X. C ) = ( B X. C ) )