Theorem undif3VD 44906

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

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 4128	. . . . . 6 ⊢ (𝑥 ∈ (𝐴 ∪ (𝐵 ∖ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ (𝐵 ∖ 𝐶)))
2		eldif 3936	. . . . . . 7 ⊢ (𝑥 ∈ (𝐵 ∖ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶))
3	2	orbi2i 912	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ (𝐵 ∖ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
4	1, 3	bitri 275	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∪ (𝐵 ∖ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
5		idn1 44599	. . . . . . . . . 10 ⊢ (   𝑥 ∈ 𝐴   ▶   𝑥 ∈ 𝐴   )
6		orc 867	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
7	5, 6	e1a 44652	. . . . . . . . 9 ⊢ (   𝑥 ∈ 𝐴   ▶   (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)   )
8		olc 868	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐴 → (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴))
9	5, 8	e1a 44652	. . . . . . . . 9 ⊢ (   𝑥 ∈ 𝐴   ▶   (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)   )
10		pm3.2 469	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) → ((¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴))))
11	7, 9, 10	e11 44713	. . . . . . . 8 ⊢ (   𝑥 ∈ 𝐴   ▶   ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴))   )
12	11	in1 44596	. . . . . . 7 ⊢ (𝑥 ∈ 𝐴 → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)))
13		idn1 44599	. . . . . . . . . . 11 ⊢ (   (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)   ▶   (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)   )
14		simpl 482	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) → 𝑥 ∈ 𝐵)
15	13, 14	e1a 44652	. . . . . . . . . 10 ⊢ (   (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)   ▶   𝑥 ∈ 𝐵   )
16		olc 868	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐵 → (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
17	15, 16	e1a 44652	. . . . . . . . 9 ⊢ (   (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)   ▶   (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)   )
18		simpr 484	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) → ¬ 𝑥 ∈ 𝐶)
19	13, 18	e1a 44652	. . . . . . . . . 10 ⊢ (   (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)   ▶    ¬ 𝑥 ∈ 𝐶   )
20		orc 867	. . . . . . . . . 10 ⊢ (¬ 𝑥 ∈ 𝐶 → (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴))
21	19, 20	e1a 44652	. . . . . . . . 9 ⊢ (   (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)   ▶   (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)   )
22	17, 21, 10	e11 44713	. . . . . . . 8 ⊢ (   (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)   ▶   ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴))   )
23	22	in1 44596	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)))
24	12, 23	jaoi 857	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)) → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)))
25		anddi 1012	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)) ↔ (((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶) ∨ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∨ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) ∨ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴))))
26	25	bicomi 224	. . . . . . 7 ⊢ ((((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶) ∨ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∨ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) ∨ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴))) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)))
27		idn1 44599	. . . . . . . . . . 11 ⊢ (   (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶)   ▶   (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶)   )
28		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶) → 𝑥 ∈ 𝐴)
29	28	orcd 873	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
30	27, 29	e1a 44652	. . . . . . . . . 10 ⊢ (   (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶)   ▶   (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶))   )
31	30	in1 44596	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
32		idn1 44599	. . . . . . . . . . . 12 ⊢ (   (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)   ▶   (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)   )
33		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
34	32, 33	e1a 44652	. . . . . . . . . . 11 ⊢ (   (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)   ▶   𝑥 ∈ 𝐴   )
35		orc 867	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
36	34, 35	e1a 44652	. . . . . . . . . 10 ⊢ (   (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)   ▶   (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶))   )
37	36	in1 44596	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
38	31, 37	jaoi 857	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶) ∨ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
39		olc 868	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
40	13, 39	e1a 44652	. . . . . . . . . 10 ⊢ (   (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)   ▶   (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶))   )
41	40	in1 44596	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
42		idn1 44599	. . . . . . . . . . . 12 ⊢ (   (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)   ▶   (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)   )
43		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
44	42, 43	e1a 44652	. . . . . . . . . . 11 ⊢ (   (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)   ▶   𝑥 ∈ 𝐴   )
45	44, 35	e1a 44652	. . . . . . . . . 10 ⊢ (   (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)   ▶   (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶))   )
46	45	in1 44596	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
47	41, 46	jaoi 857	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) ∨ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)) → (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
48	38, 47	jaoi 857	. . . . . . 7 ⊢ ((((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶) ∨ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∨ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) ∨ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴))) → (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
49	26, 48	sylbir 235	. . . . . 6 ⊢ (((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)) → (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
50	24, 49	impbii 209	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)))
51	4, 50	bitri 275	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∪ (𝐵 ∖ 𝐶)) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)))
52		eldif 3936	. . . . 5 ⊢ (𝑥 ∈ ((𝐴 ∪ 𝐵) ∖ (𝐶 ∖ 𝐴)) ↔ (𝑥 ∈ (𝐴 ∪ 𝐵) ∧ ¬ 𝑥 ∈ (𝐶 ∖ 𝐴)))
53		elun 4128	. . . . . 6 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
54		eldif 3936	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐶 ∖ 𝐴) ↔ (𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐴))
55	54	notbii 320	. . . . . . 7 ⊢ (¬ 𝑥 ∈ (𝐶 ∖ 𝐴) ↔ ¬ (𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐴))
56		pm4.53 987	. . . . . . 7 ⊢ (¬ (𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐴) ↔ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴))
57	55, 56	bitri 275	. . . . . 6 ⊢ (¬ 𝑥 ∈ (𝐶 ∖ 𝐴) ↔ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴))
58	53, 57	anbi12i 628	. . . . 5 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ∧ ¬ 𝑥 ∈ (𝐶 ∖ 𝐴)) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)))
59	52, 58	bitri 275	. . . 4 ⊢ (𝑥 ∈ ((𝐴 ∪ 𝐵) ∖ (𝐶 ∖ 𝐴)) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)))
60	51, 59	bitr4i 278	. . 3 ⊢ (𝑥 ∈ (𝐴 ∪ (𝐵 ∖ 𝐶)) ↔ 𝑥 ∈ ((𝐴 ∪ 𝐵) ∖ (𝐶 ∖ 𝐴)))
61	60	ax-gen 1795	. 2 ⊢ ∀𝑥(𝑥 ∈ (𝐴 ∪ (𝐵 ∖ 𝐶)) ↔ 𝑥 ∈ ((𝐴 ∪ 𝐵) ∖ (𝐶 ∖ 𝐴)))
62		dfcleq 2728	. . 3 ⊢ ((𝐴 ∪ (𝐵 ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ (𝐶 ∖ 𝐴)) ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ (𝐵 ∖ 𝐶)) ↔ 𝑥 ∈ ((𝐴 ∪ 𝐵) ∖ (𝐶 ∖ 𝐴))))
63	62	biimpri 228	. 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ (𝐵 ∖ 𝐶)) ↔ 𝑥 ∈ ((𝐴 ∪ 𝐵) ∖ (𝐶 ∖ 𝐴))) → (𝐴 ∪ (𝐵 ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ (𝐶 ∖ 𝐴)))
64	61, 63	e0a 44796	1 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ (𝐶 ∖ 𝐴))

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   ∨ wo 847  ∀wal 1538   = wceq 1540   ∈ wcel 2108   ∖ cdif 3923   ∪ cun 3924

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-dif 3929  df-un 3931  df-vd1 44595

This theorem is referenced by: (None)