Theorem undif3VD 43945

Description: The first equality of Exercise 13 of [TakeutiZaring] p. 22. Virtual deduction proof of undif3 4290. 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 4290 is undif3VD 43945 without virtual deductions and was automatically derived from undif3VD 43945.

1::	⊢ (𝑥 ∈ (𝐴 ∪ (𝐵 ∖ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ (𝐵 ∖ 𝐶)))
2::	⊢ (𝑥 ∈ (𝐵 ∖ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶))
3:2:	⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ (𝐵 ∖ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
4:1,3:	⊢ (𝑥 ∈ (𝐴 ∪ (𝐵 ∖ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
5::	⊢ (   𝑥 ∈ 𝐴   ▶   𝑥 ∈ 𝐴   )
6:5:	⊢ (   𝑥 ∈ 𝐴   ▶   (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)   )
7:5:	⊢ (   𝑥 ∈ 𝐴   ▶   (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)   )
8:6,7:	⊢ (   𝑥 ∈ 𝐴   ▶   ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴))   )
9:8:	⊢ (𝑥 ∈ 𝐴 → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ ( ¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)))
10::	⊢ (   (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)   ▶   (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)   )
11:10:	⊢ (   (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)   ▶   𝑥 ∈ 𝐵   )
12:10:	⊢ (   (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)   ▶   ¬ 𝑥 ∈ 𝐶    )
13:11:	⊢ (   (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)   ▶   (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)   )
14:12:	⊢ (   (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)   ▶   (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)   )
15:13,14:	⊢ (   (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)   ▶   ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴))   )
16:15:	⊢ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)))
17:9,16:	⊢ ((𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)) → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)))
18::	⊢ (   (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶)   ▶   (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶)   )
19:18:	⊢ (   (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶)   ▶   𝑥 ∈ 𝐴   )
20:18:	⊢ (   (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶)   ▶   ¬ 𝑥 ∈ 𝐶    )
21:18:	⊢ (   (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶)   ▶   (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶))   )
22:21:	⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
23::	⊢ (   (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)   ▶   (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)   )
24:23:	⊢ (   (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)   ▶   𝑥 ∈ 𝐴   )
25:24:	⊢ (   (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)   ▶   (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶))   )
26:25:	⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐴 ∨ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
27:10:	⊢ (   (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)   ▶   (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶))   )
28:27:	⊢ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
29::	⊢ (   (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)   ▶   (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)   )
30:29:	⊢ (   (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)   ▶   𝑥 ∈ 𝐴   )
31:30:	⊢ (   (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)   ▶   (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶))   )
32:31:	⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐴 ∨ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
33:22,26:	⊢ (((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶) ∨ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
34:28,32:	⊢ (((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) ∨ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)) → (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
35:33,34:	⊢ ((((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶) ∨ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∨ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) ∨ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴))) → (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
36::	⊢ ((((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶) ∨ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∨ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) ∨ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴))) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)))
37:36,35:	⊢ (((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)) → (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
38:17,37:	⊢ ((𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)))
39::	⊢ (𝑥 ∈ (𝐶 ∖ 𝐴) ↔ (𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐴))
40:39:	⊢ (¬ 𝑥 ∈ (𝐶 ∖ 𝐴) ↔ ¬ (𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐴))
41::	⊢ (¬ (𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐴) ↔ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴))
42:40,41:	⊢ (¬ 𝑥 ∈ (𝐶 ∖ 𝐴) ↔ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴))
43::	⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ))
44:43,42:	⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ∧ ¬ 𝑥 ∈ (𝐶 ∖ 𝐴) ) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴)))
45::	⊢ (𝑥 ∈ ((𝐴 ∪ 𝐵) ∖ (𝐶 ∖ 𝐴)) ↔ ( 𝑥 ∈ (𝐴 ∪ 𝐵) ∧ ¬ 𝑥 ∈ (𝐶 ∖ 𝐴)))
46:45,44:	⊢ (𝑥 ∈ ((𝐴 ∪ 𝐵) ∖ (𝐶 ∖ 𝐴)) ↔ ( (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)))
47:4,38:	⊢ (𝑥 ∈ (𝐴 ∪ (𝐵 ∖ 𝐶)) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)))
48:46,47:	⊢ (𝑥 ∈ (𝐴 ∪ (𝐵 ∖ 𝐶)) ↔ 𝑥 ∈ ((𝐴 ∪ 𝐵) ∖ (𝐶 ∖ 𝐴)))
49:48:	⊢ ∀𝑥(𝑥 ∈ (𝐴 ∪ (𝐵 ∖ 𝐶)) ↔ 𝑥 ∈ ((𝐴 ∪ 𝐵) ∖ (𝐶 ∖ 𝐴)))
qed:49:	⊢ (𝐴 ∪ (𝐵 ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ (𝐶 ∖ 𝐴))

(Contributed by Alan Sare, 17-Apr-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

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

Proof of Theorem undif3VD

Dummy variable 𝑥 is distinct from all other variables.

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

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 396   ∨ wo 845  ∀wal 1539   = wceq 1541   ∈ wcel 2106   ∖ cdif 3945   ∪ cun 3946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-dif 3951  df-un 3953  df-vd1 43633

This theorem is referenced by: (None)