Description: Equality theorem for Cartesian product. (Contributed by NM, 4-Jul-1994)
Ref | Expression | ||
---|---|---|---|
Assertion | xpeq1 | |- ( A = B -> ( A X. C ) = ( B X. C ) ) |
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 ) ) |