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 ) )