Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
The difference, union, and intersection of two classes
The intersection of two classes
ineq12
Next ⟩
ineq1i
Metamath Proof Explorer
Ascii
Unicode
Theorem
ineq12
Description:
Equality theorem for intersection of two classes.
(Contributed by
NM
, 8-May-1994)
Ref
Expression
Assertion
ineq12
⊢
A
=
B
∧
C
=
D
→
A
∩
C
=
B
∩
D
Proof
Step
Hyp
Ref
Expression
1
ineq1
⊢
A
=
B
→
A
∩
C
=
B
∩
C
2
ineq2
⊢
C
=
D
→
B
∩
C
=
B
∩
D
3
1
2
sylan9eq
⊢
A
=
B
∧
C
=
D
→
A
∩
C
=
B
∩
D