Theorem undif3VD 40768

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

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 4048	. . . . . 6 ⊢ (𝑥 ∈ (𝐴 ∪ (𝐵 ∖ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ (𝐵 ∖ 𝐶)))
2		eldif 3871	. . . . . . 7 ⊢ (𝑥 ∈ (𝐵 ∖ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶))
3	2	orbi2i 907	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ (𝐵 ∖ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
4	1, 3	bitri 276	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∪ (𝐵 ∖ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
5		idn1 40460	. . . . . . . . . 10 ⊢ (   𝑥 ∈ 𝐴   ▶   𝑥 ∈ 𝐴   )
6		orc 862	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
7	5, 6	e1a 40513	. . . . . . . . 9 ⊢ (   𝑥 ∈ 𝐴   ▶   (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)   )
8		olc 863	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐴 → (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴))
9	5, 8	e1a 40513	. . . . . . . . 9 ⊢ (   𝑥 ∈ 𝐴   ▶   (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)   )
10		pm3.2 470	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) → ((¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴))))
11	7, 9, 10	e11 40574	. . . . . . . 8 ⊢ (   𝑥 ∈ 𝐴   ▶   ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴))   )
12	11	in1 40457	. . . . . . 7 ⊢ (𝑥 ∈ 𝐴 → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)))
13		idn1 40460	. . . . . . . . . . 11 ⊢ (   (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)   ▶   (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)   )
14		simpl 483	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) → 𝑥 ∈ 𝐵)
15	13, 14	e1a 40513	. . . . . . . . . 10 ⊢ (   (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)   ▶   𝑥 ∈ 𝐵   )
16		olc 863	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐵 → (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
17	15, 16	e1a 40513	. . . . . . . . 9 ⊢ (   (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)   ▶   (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)   )
18		simpr 485	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) → ¬ 𝑥 ∈ 𝐶)
19	13, 18	e1a 40513	. . . . . . . . . 10 ⊢ (   (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)   ▶    ¬ 𝑥 ∈ 𝐶   )
20		orc 862	. . . . . . . . . 10 ⊢ (¬ 𝑥 ∈ 𝐶 → (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴))
21	19, 20	e1a 40513	. . . . . . . . 9 ⊢ (   (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)   ▶   (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)   )
22	17, 21, 10	e11 40574	. . . . . . . 8 ⊢ (   (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)   ▶   ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴))   )
23	22	in1 40457	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)))
24	12, 23	jaoi 852	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)) → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)))
25		anddi 1005	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)) ↔ (((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶) ∨ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∨ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) ∨ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴))))
26	25	bicomi 225	. . . . . . 7 ⊢ ((((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶) ∨ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∨ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) ∨ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴))) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)))
27		idn1 40460	. . . . . . . . . . 11 ⊢ (   (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶)   ▶   (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶)   )
28		simpl 483	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶) → 𝑥 ∈ 𝐴)
29	28	orcd 870	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
30	27, 29	e1a 40513	. . . . . . . . . 10 ⊢ (   (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶)   ▶   (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶))   )
31	30	in1 40457	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
32		idn1 40460	. . . . . . . . . . . 12 ⊢ (   (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)   ▶   (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)   )
33		simpl 483	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
34	32, 33	e1a 40513	. . . . . . . . . . 11 ⊢ (   (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)   ▶   𝑥 ∈ 𝐴   )
35		orc 862	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
36	34, 35	e1a 40513	. . . . . . . . . 10 ⊢ (   (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)   ▶   (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶))   )
37	36	in1 40457	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
38	31, 37	jaoi 852	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶) ∨ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
39		olc 863	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
40	13, 39	e1a 40513	. . . . . . . . . 10 ⊢ (   (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)   ▶   (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶))   )
41	40	in1 40457	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
42		idn1 40460	. . . . . . . . . . . 12 ⊢ (   (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)   ▶   (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)   )
43		simpr 485	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
44	42, 43	e1a 40513	. . . . . . . . . . 11 ⊢ (   (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)   ▶   𝑥 ∈ 𝐴   )
45	44, 35	e1a 40513	. . . . . . . . . 10 ⊢ (   (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)   ▶   (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶))   )
46	45	in1 40457	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
47	41, 46	jaoi 852	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) ∨ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)) → (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
48	38, 47	jaoi 852	. . . . . . 7 ⊢ ((((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶) ∨ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∨ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) ∨ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴))) → (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
49	26, 48	sylbir 236	. . . . . 6 ⊢ (((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)) → (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
50	24, 49	impbii 210	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)))
51	4, 50	bitri 276	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∪ (𝐵 ∖ 𝐶)) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)))
52		eldif 3871	. . . . 5 ⊢ (𝑥 ∈ ((𝐴 ∪ 𝐵) ∖ (𝐶 ∖ 𝐴)) ↔ (𝑥 ∈ (𝐴 ∪ 𝐵) ∧ ¬ 𝑥 ∈ (𝐶 ∖ 𝐴)))
53		elun 4048	. . . . . 6 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
54		eldif 3871	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐶 ∖ 𝐴) ↔ (𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐴))
55	54	notbii 321	. . . . . . 7 ⊢ (¬ 𝑥 ∈ (𝐶 ∖ 𝐴) ↔ ¬ (𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐴))
56		pm4.53 980	. . . . . . 7 ⊢ (¬ (𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐴) ↔ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴))
57	55, 56	bitri 276	. . . . . 6 ⊢ (¬ 𝑥 ∈ (𝐶 ∖ 𝐴) ↔ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴))
58	53, 57	anbi12i 626	. . . . 5 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ∧ ¬ 𝑥 ∈ (𝐶 ∖ 𝐴)) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)))
59	52, 58	bitri 276	. . . 4 ⊢ (𝑥 ∈ ((𝐴 ∪ 𝐵) ∖ (𝐶 ∖ 𝐴)) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)))
60	51, 59	bitr4i 279	. . 3 ⊢ (𝑥 ∈ (𝐴 ∪ (𝐵 ∖ 𝐶)) ↔ 𝑥 ∈ ((𝐴 ∪ 𝐵) ∖ (𝐶 ∖ 𝐴)))
61	60	ax-gen 1778	. 2 ⊢ ∀𝑥(𝑥 ∈ (𝐴 ∪ (𝐵 ∖ 𝐶)) ↔ 𝑥 ∈ ((𝐴 ∪ 𝐵) ∖ (𝐶 ∖ 𝐴)))
62		dfcleq 2788	. . 3 ⊢ ((𝐴 ∪ (𝐵 ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ (𝐶 ∖ 𝐴)) ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ (𝐵 ∖ 𝐶)) ↔ 𝑥 ∈ ((𝐴 ∪ 𝐵) ∖ (𝐶 ∖ 𝐴))))
63	62	biimpri 229	. 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ (𝐵 ∖ 𝐶)) ↔ 𝑥 ∈ ((𝐴 ∪ 𝐵) ∖ (𝐶 ∖ 𝐴))) → (𝐴 ∪ (𝐵 ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ (𝐶 ∖ 𝐴)))
64	61, 63	e0a 40658	1 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ (𝐶 ∖ 𝐴))

Syntax hints:  ¬ wn 3   ↔ wb 207   ∧ wa 396   ∨ wo 842  ∀wal 1520   = wceq 1522   ∈ wcel 2080   ∖ cdif 3858   ∪ cun 3859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-8 2082  ax-9 2090  ax-10 2111  ax-11 2125  ax-12 2140  ax-ext 2768

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1763  df-nf 1767  df-sb 2042  df-clab 2775  df-cleq 2787  df-clel 2862  df-nfc 2934  df-v 3438  df-dif 3864  df-un 3866  df-vd1 40456

This theorem is referenced by: (None)