Metamath Proof Explorer

Theorem indif2

Description: Bring an intersection in and out of a class difference. (Contributed by Jeff Hankins, 15-Jul-2009)

Ref Expression
Assertion indif2 A B C = A B C


Step Hyp Ref Expression
1 inass A B V C = A B V C
2 invdif A B V C = A B C
3 invdif B V C = B C
4 3 ineq2i A B V C = A B C
5 1 2 4 3eqtr3ri A B C = A B C