Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Relations
xpeq2
Next ⟩
elxpi
Metamath Proof Explorer
Ascii
Unicode
Theorem
xpeq2
Description:
Equality theorem for Cartesian product.
(Contributed by
NM
, 5-Jul-1994)
Ref
Expression
Assertion
xpeq2
⊢
A
=
B
→
C
×
A
=
C
×
B
Proof
Step
Hyp
Ref
Expression
1
eleq2
⊢
A
=
B
→
y
∈
A
↔
y
∈
B
2
1
anbi2d
⊢
A
=
B
→
x
∈
C
∧
y
∈
A
↔
x
∈
C
∧
y
∈
B
3
2
opabbidv
⊢
A
=
B
→
x
y
|
x
∈
C
∧
y
∈
A
=
x
y
|
x
∈
C
∧
y
∈
B
4
df-xp
⊢
C
×
A
=
x
y
|
x
∈
C
∧
y
∈
A
5
df-xp
⊢
C
×
B
=
x
y
|
x
∈
C
∧
y
∈
B
6
3
4
5
3eqtr4g
⊢
A
=
B
→
C
×
A
=
C
×
B