Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Relations
xpdisj2
Next ⟩
xpsndisj
Metamath Proof Explorer
Ascii
Unicode
Theorem
xpdisj2
Description:
Cartesian products with disjoint sets are disjoint.
(Contributed by
NM
, 13-Sep-2004)
Ref
Expression
Assertion
xpdisj2
⊢
A
∩
B
=
∅
→
C
×
A
∩
D
×
B
=
∅
Proof
Step
Hyp
Ref
Expression
1
xpeq2
⊢
A
∩
B
=
∅
→
C
∩
D
×
A
∩
B
=
C
∩
D
×
∅
2
inxp
⊢
C
×
A
∩
D
×
B
=
C
∩
D
×
A
∩
B
3
xp0
⊢
C
∩
D
×
∅
=
∅
4
3
eqcomi
⊢
∅
=
C
∩
D
×
∅
5
1
2
4
3eqtr4g
⊢
A
∩
B
=
∅
→
C
×
A
∩
D
×
B
=
∅