undif3VD

Description: The first equality of Exercise 13 of TakeutiZaring p. 22. Virtual deduction proof of undif3 . The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. undif3 is undif3VD without virtual deductions and was automatically derived from undif3VD .

		Ref	Expression
	Assertion	undif3VD	⊢ ( 𝐴 ∪ ( 𝐵 ∖ 𝐶 ) ) = ( ( 𝐴 ∪ 𝐵 ) ∖ ( 𝐶 ∖ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		elun	⊢ ( 𝑥 ∈ ( 𝐴 ∪ ( 𝐵 ∖ 𝐶 ) ) ↔ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ) )
2		eldif	⊢ ( 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) )
3	2	orbi2i	⊢ ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ) ↔ ( 𝑥 ∈ 𝐴 ∨ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) )
4	1 3	bitri	⊢ ( 𝑥 ∈ ( 𝐴 ∪ ( 𝐵 ∖ 𝐶 ) ) ↔ ( 𝑥 ∈ 𝐴 ∨ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) )
5		idn1	⊢ ( 𝑥 ∈ 𝐴 ▶ 𝑥 ∈ 𝐴 )
6		orc	⊢ ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) )
7	5 6	e1a	⊢ ( 𝑥 ∈ 𝐴 ▶ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) )
8		olc	⊢ ( 𝑥 ∈ 𝐴 → ( ¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴 ) )
9	5 8	e1a	⊢ ( 𝑥 ∈ 𝐴 ▶ ( ¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴 ) )
10		pm3.2	⊢ ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) → ( ( ¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ∧ ( ¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴 ) ) ) )
11	7 9 10	e11	⊢ ( 𝑥 ∈ 𝐴 ▶ ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ∧ ( ¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴 ) ) )
12	11	in1	⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ∧ ( ¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴 ) ) )
13		idn1	⊢ ( ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ▶ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) )
14		simpl	⊢ ( ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ 𝐵 )
15	13 14	e1a	⊢ ( ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ▶ 𝑥 ∈ 𝐵 )
16		olc	⊢ ( 𝑥 ∈ 𝐵 → ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) )
17	15 16	e1a	⊢ ( ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ▶ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) )
18		simpr	⊢ ( ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) → ¬ 𝑥 ∈ 𝐶 )
19	13 18	e1a	⊢ ( ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ▶ ¬ 𝑥 ∈ 𝐶 )
20		orc	⊢ ( ¬ 𝑥 ∈ 𝐶 → ( ¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴 ) )
21	19 20	e1a	⊢ ( ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ▶ ( ¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴 ) )
22	17 21 10	e11	⊢ ( ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ▶ ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ∧ ( ¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴 ) ) )
23	22	in1	⊢ ( ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) → ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ∧ ( ¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴 ) ) )
24	12 23	jaoi	⊢ ( ( 𝑥 ∈ 𝐴 ∨ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) → ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ∧ ( ¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴 ) ) )
25		anddi	⊢ ( ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ∧ ( ¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴 ) ) ↔ ( ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶 ) ∨ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) ∨ ( ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ∨ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ) ) )
26	25	bicomi	⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶 ) ∨ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) ∨ ( ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ∨ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ∧ ( ¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴 ) ) )
27		idn1	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶 ) ▶ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶 ) )
28		simpl	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ 𝐴 )
29	28	orcd	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶 ) → ( 𝑥 ∈ 𝐴 ∨ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) )
30	27 29	e1a	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶 ) ▶ ( 𝑥 ∈ 𝐴 ∨ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) )
31	30	in1	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶 ) → ( 𝑥 ∈ 𝐴 ∨ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) )
32		idn1	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ▶ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) )
33		simpl	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
34	32 33	e1a	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ▶ 𝑥 ∈ 𝐴 )
35		orc	⊢ ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 ∨ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) )
36	34 35	e1a	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ▶ ( 𝑥 ∈ 𝐴 ∨ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) )
37	36	in1	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ 𝐴 ∨ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) )
38	31 37	jaoi	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶 ) ∨ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) → ( 𝑥 ∈ 𝐴 ∨ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) )
39		olc	⊢ ( ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) → ( 𝑥 ∈ 𝐴 ∨ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) )
40	13 39	e1a	⊢ ( ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ▶ ( 𝑥 ∈ 𝐴 ∨ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) )
41	40	in1	⊢ ( ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) → ( 𝑥 ∈ 𝐴 ∨ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) )
42		idn1	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ▶ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) )
43		simpr	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
44	42 43	e1a	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ▶ 𝑥 ∈ 𝐴 )
45	44 35	e1a	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ▶ ( 𝑥 ∈ 𝐴 ∨ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) )
46	45	in1	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ 𝐴 ∨ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) )
47	41 46	jaoi	⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ∨ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ) → ( 𝑥 ∈ 𝐴 ∨ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) )
48	38 47	jaoi	⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶 ) ∨ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) ∨ ( ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ∨ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ) ) → ( 𝑥 ∈ 𝐴 ∨ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) )
49	26 48	sylbir	⊢ ( ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ∧ ( ¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴 ) ) → ( 𝑥 ∈ 𝐴 ∨ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) )
50	24 49	impbii	⊢ ( ( 𝑥 ∈ 𝐴 ∨ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ∧ ( ¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴 ) ) )
51	4 50	bitri	⊢ ( 𝑥 ∈ ( 𝐴 ∪ ( 𝐵 ∖ 𝐶 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ∧ ( ¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴 ) ) )
52		eldif	⊢ ( 𝑥 ∈ ( ( 𝐴 ∪ 𝐵 ) ∖ ( 𝐶 ∖ 𝐴 ) ) ↔ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∧ ¬ 𝑥 ∈ ( 𝐶 ∖ 𝐴 ) ) )
53		elun	⊢ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) )
54		eldif	⊢ ( 𝑥 ∈ ( 𝐶 ∖ 𝐴 ) ↔ ( 𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐴 ) )
55	54	notbii	⊢ ( ¬ 𝑥 ∈ ( 𝐶 ∖ 𝐴 ) ↔ ¬ ( 𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐴 ) )
56		pm4.53	⊢ ( ¬ ( 𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐴 ) ↔ ( ¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴 ) )
57	55 56	bitri	⊢ ( ¬ 𝑥 ∈ ( 𝐶 ∖ 𝐴 ) ↔ ( ¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴 ) )
58	53 57	anbi12i	⊢ ( ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∧ ¬ 𝑥 ∈ ( 𝐶 ∖ 𝐴 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ∧ ( ¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴 ) ) )
59	52 58	bitri	⊢ ( 𝑥 ∈ ( ( 𝐴 ∪ 𝐵 ) ∖ ( 𝐶 ∖ 𝐴 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ∧ ( ¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴 ) ) )
60	51 59	bitr4i	⊢ ( 𝑥 ∈ ( 𝐴 ∪ ( 𝐵 ∖ 𝐶 ) ) ↔ 𝑥 ∈ ( ( 𝐴 ∪ 𝐵 ) ∖ ( 𝐶 ∖ 𝐴 ) ) )
61	60	ax-gen	⊢ ∀ 𝑥 ( 𝑥 ∈ ( 𝐴 ∪ ( 𝐵 ∖ 𝐶 ) ) ↔ 𝑥 ∈ ( ( 𝐴 ∪ 𝐵 ) ∖ ( 𝐶 ∖ 𝐴 ) ) )
62		dfcleq	⊢ ( ( 𝐴 ∪ ( 𝐵 ∖ 𝐶 ) ) = ( ( 𝐴 ∪ 𝐵 ) ∖ ( 𝐶 ∖ 𝐴 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ ( 𝐴 ∪ ( 𝐵 ∖ 𝐶 ) ) ↔ 𝑥 ∈ ( ( 𝐴 ∪ 𝐵 ) ∖ ( 𝐶 ∖ 𝐴 ) ) ) )
63	62	biimpri	⊢ ( ∀ 𝑥 ( 𝑥 ∈ ( 𝐴 ∪ ( 𝐵 ∖ 𝐶 ) ) ↔ 𝑥 ∈ ( ( 𝐴 ∪ 𝐵 ) ∖ ( 𝐶 ∖ 𝐴 ) ) ) → ( 𝐴 ∪ ( 𝐵 ∖ 𝐶 ) ) = ( ( 𝐴 ∪ 𝐵 ) ∖ ( 𝐶 ∖ 𝐴 ) ) )
64	61 63	e0a	⊢ ( 𝐴 ∪ ( 𝐵 ∖ 𝐶 ) ) = ( ( 𝐴 ∪ 𝐵 ) ∖ ( 𝐶 ∖ 𝐴 ) )

1::	\|- ( x e. ( A u. ( B \ C ) ) <-> ( x e. A \/ x e. ( B \ C ) ) )
2::	\|- ( x e. ( B \ C ) <-> ( x e. B /\ -. x e. C ) )
3:2:	\|- ( ( x e. A \/ x e. ( B \ C ) ) <-> ( x e. A \/ ( x e. B /\ -. x e. C ) ) )
4:1,3:	\|- ( x e. ( A u. ( B \ C ) ) <-> ( x e. A \/ ( x e. B /\ -. x e. C ) ) )
5::	\|- (. x e. A ->. x e. A ).
6:5:	\|- (. x e. A ->. ( x e. A \/ x e. B ) ).
7:5:	\|- (. x e. A ->. ( -. x e. C \/ x e. A ) ).
8:6,7:	\|- (. x e. A ->. ( ( x e. A \/ x e. B ) /\ ( -. x e. C \/ x e. A ) ) ).
9:8:	\|- ( x e. A -> ( ( x e. A \/ x e. B ) /\ ( -. x e. C \/ x e. A ) ) )
10::	\|- (. ( x e. B /\ -. x e. C ) ->. ( x e. B /\ -. x e. C ) ).
11:10:	\|- (. ( x e. B /\ -. x e. C ) ->. x e. B ).
12:10:	\|- (. ( x e. B /\ -. x e. C ) ->. -. x e. C ).
13:11:	\|- (. ( x e. B /\ -. x e. C ) ->. ( x e. A \/ x e. B ) ).
14:12:	\|- (. ( x e. B /\ -. x e. C ) ->. ( -. x e. C \/ x e. A ) ).
15:13,14:	\|- (. ( x e. B /\ -. x e. C ) ->. ( ( x e. A \/ x e. B ) /\ ( -. x e. C \/ x e. A ) ) ).
16:15:	\|- ( ( x e. B /\ -. x e. C ) -> ( ( x e. A \/ x e. B ) /\ ( -. x e. C \/ x e. A ) ) )
17:9,16:	\|- ( ( x e. A \/ ( x e. B /\ -. x e. C ) ) -> ( ( x e. A \/ x e. B ) /\ ( -. x e. C \/ x e. A ) ) )
18::	\|- (. ( x e. A /\ -. x e. C ) ->. ( x e. A /\ -. x e. C ) ).
19:18:	\|- (. ( x e. A /\ -. x e. C ) ->. x e. A ).
20:18:	\|- (. ( x e. A /\ -. x e. C ) ->. -. x e. C ).
21:18:	\|- (. ( x e. A /\ -. x e. C ) ->. ( x e. A \/ ( x e. B /\ -. x e. C ) ) ).
22:21:	\|- ( ( x e. A /\ -. x e. C ) -> ( x e. A \/ ( x e. B /\ -. x e. C ) ) )
23::	\|- (. ( x e. A /\ x e. A ) ->. ( x e. A /\ x e. A ) ).
24:23:	\|- (. ( x e. A /\ x e. A ) ->. x e. A ).
25:24:	\|- (. ( x e. A /\ x e. A ) ->. ( x e. A \/ ( x e. B /\ -. x e. C ) ) ).
26:25:	\|- ( ( x e. A /\ x e. A ) -> ( x e. A \/ ( x e. B /\ -. x e. C ) ) )
27:10:	\|- (. ( x e. B /\ -. x e. C ) ->. ( x e. A \/ ( x e. B /\ -. x e. C ) ) ).
28:27:	\|- ( ( x e. B /\ -. x e. C ) -> ( x e. A \/ ( x e. B /\ -. x e. C ) ) )
29::	\|- (. ( x e. B /\ x e. A ) ->. ( x e. B /\ x e. A ) ).
30:29:	\|- (. ( x e. B /\ x e. A ) ->. x e. A ).
31:30:	\|- (. ( x e. B /\ x e. A ) ->. ( x e. A \/ ( x e. B /\ -. x e. C ) ) ).
32:31:	\|- ( ( x e. B /\ x e. A ) -> ( x e. A \/ ( x e. B /\ -. x e. C ) ) )
33:22,26:	\|- ( ( ( x e. A /\ -. x e. C ) \/ ( x e. A /\ x e. A ) ) -> ( x e. A \/ ( x e. B /\ -. x e. C ) ) )
34:28,32:	\|- ( ( ( x e. B /\ -. x e. C ) \/ ( x e. B /\ x e. A ) ) -> ( x e. A \/ ( x e. B /\ -. x e. C ) ) )
35:33,34:	\|- ( ( ( ( x e. A /\ -. x e. C ) \/ ( x e. A /\ x e. A ) ) \/ ( ( x e. B /\ -. x e. C ) \/ ( x e. B /\ x e. A ) ) ) -> ( x e. A \/ ( x e. B /\ -. x e. C ) ) )
36::	\|- ( ( ( ( x e. A /\ -. x e. C ) \/ ( x e. A /\ x e. A ) ) \/ ( ( x e. B /\ -. x e. C ) \/ ( x e. B /\ x e. A ) ) ) <-> ( ( x e. A \/ x e. B ) /\ ( -. x e. C \/ x e. A ) ) )
37:36,35:	\|- ( ( ( x e. A \/ x e. B ) /\ ( -. x e. C \/ x e. A ) ) -> ( x e. A \/ ( x e. B /\ -. x e. C ) ) )
38:17,37:	\|- ( ( x e. A \/ ( x e. B /\ -. x e. C ) ) <-> ( ( x e. A \/ x e. B ) /\ ( -. x e. C \/ x e. A ) ) )
39::	\|- ( x e. ( C \ A ) <-> ( x e. C /\ -. x e. A ) )
40:39:	\|- ( -. x e. ( C \ A ) <-> -. ( x e. C /\ -. x e. A ) )
41::	\|- ( -. ( x e. C /\ -. x e. A ) <-> ( -. x e. C \/ x e. A ) )
42:40,41:	\|- ( -. x e. ( C \ A ) <-> ( -. x e. C \/ x e. A ) )
43::	\|- ( x e. ( A u. B ) <-> ( x e. A \/ x e. B ) )
44:43,42:	\|- ( ( x e. ( A u. B ) /\ -. x e. ( C \ A ) ) <-> ( ( x e. A \/ x e. B ) /\ ( -. x e. C /\ x e. A ) ) )
45::	\|- ( x e. ( ( A u. B ) \ ( C \ A ) ) <-> ( x e. ( A u. B ) /\ -. x e. ( C \ A ) ) )
46:45,44:	\|- ( x e. ( ( A u. B ) \ ( C \ A ) ) <-> ( ( x e. A \/ x e. B ) /\ ( -. x e. C \/ x e. A ) ) )
47:4,38:	\|- ( x e. ( A u. ( B \ C ) ) <-> ( ( x e. A \/ x e. B ) /\ ( -. x e. C \/ x e. A ) ) )
48:46,47:	\|- ( x e. ( A u. ( B \ C ) ) <-> x e. ( ( A u. B ) \ ( C \ A ) ) )
49:48:	\|- A. x ( x e. ( A u. ( B \ C ) ) <-> x e. ( ( A u. B ) \ ( C \ A ) ) )
qed:49:	\|- ( A u. ( B \ C ) ) = ( ( A u. B ) \ ( C \ A ) )

Metamath Proof Explorer

Theorem undif3VD

Proof