Metamath Proof Explorer


Theorem ineq2

Description: Equality theorem for intersection of two classes. (Contributed by NM, 26-Dec-1993)

Ref Expression
Assertion ineq2 A=BCA=CB

Proof

Step Hyp Ref Expression
1 ineq1 A=BAC=BC
2 incom CA=AC
3 incom CB=BC
4 1 2 3 3eqtr4g A=BCA=CB