This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem undif3

Description: An equality involving class union and class difference. The first equality of Exercise 13 of TakeutiZaring p. 22. (Contributed by Alan Sare, 17-Apr-2012) (Proof shortened by JJ, 13-Jul-2021)

Ref Expression
Assertion undif3 
|- ( A u. ( B \ C ) ) = ( ( A u. B ) \ ( C \ A ) )

Proof

Step Hyp Ref Expression
1 elun 
 |-  ( x e. ( A u. B ) <-> ( x e. A \/ x e. B ) )
2 pm4.53 
 |-  ( -. ( x e. C /\ -. x e. A ) <-> ( -. x e. C \/ x e. A ) )
3 eldif 
 |-  ( x e. ( C \ A ) <-> ( x e. C /\ -. x e. A ) )
4 2 3 xchnxbir 
 |-  ( -. x e. ( C \ A ) <-> ( -. x e. C \/ x e. A ) )
5 1 4 anbi12i 
 |-  ( ( x e. ( A u. B ) /\ -. x e. ( C \ A ) ) <-> ( ( x e. A \/ x e. B ) /\ ( -. x e. C \/ x e. A ) ) )
6 eldif 
 |-  ( x e. ( ( A u. B ) \ ( C \ A ) ) <-> ( x e. ( A u. B ) /\ -. x e. ( C \ A ) ) )
7 elun 
 |-  ( x e. ( A u. ( B \ C ) ) <-> ( x e. A \/ x e. ( B \ C ) ) )
8 eldif 
 |-  ( x e. ( B \ C ) <-> ( x e. B /\ -. x e. C ) )
9 8 orbi2i 
 |-  ( ( x e. A \/ x e. ( B \ C ) ) <-> ( x e. A \/ ( x e. B /\ -. x e. C ) ) )
10 ordi 
 |-  ( ( x e. A \/ ( x e. B /\ -. x e. C ) ) <-> ( ( x e. A \/ x e. B ) /\ ( x e. A \/ -. x e. C ) ) )
11 orcom 
 |-  ( ( x e. A \/ -. x e. C ) <-> ( -. x e. C \/ x e. A ) )
12 11 anbi2i 
 |-  ( ( ( x e. A \/ x e. B ) /\ ( x e. A \/ -. x e. C ) ) <-> ( ( x e. A \/ x e. B ) /\ ( -. x e. C \/ x e. A ) ) )
13 10 12 bitri 
 |-  ( ( x e. A \/ ( x e. B /\ -. x e. C ) ) <-> ( ( x e. A \/ x e. B ) /\ ( -. x e. C \/ x e. A ) ) )
14 7 9 13 3bitri 
 |-  ( x e. ( A u. ( B \ C ) ) <-> ( ( x e. A \/ x e. B ) /\ ( -. x e. C \/ x e. A ) ) )
15 5 6 14 3bitr4ri 
 |-  ( x e. ( A u. ( B \ C ) ) <-> x e. ( ( A u. B ) \ ( C \ A ) ) )
16 15 eqriv 
 |-  ( A u. ( B \ C ) ) = ( ( A u. B ) \ ( C \ A ) )