Theorem undif3VD 44902

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

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 4153	. . . . . 6 ⊢ (𝑥 ∈ (𝐴 ∪ (𝐵 ∖ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ (𝐵 ∖ 𝐶)))
2		eldif 3961	. . . . . . 7 ⊢ (𝑥 ∈ (𝐵 ∖ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶))
3	2	orbi2i 913	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ (𝐵 ∖ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
4	1, 3	bitri 275	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∪ (𝐵 ∖ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
5		idn1 44594	. . . . . . . . . 10 ⊢ (   𝑥 ∈ 𝐴   ▶   𝑥 ∈ 𝐴   )
6		orc 868	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
7	5, 6	e1a 44647	. . . . . . . . 9 ⊢ (   𝑥 ∈ 𝐴   ▶   (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)   )
8		olc 869	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐴 → (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴))
9	5, 8	e1a 44647	. . . . . . . . 9 ⊢ (   𝑥 ∈ 𝐴   ▶   (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)   )
10		pm3.2 469	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) → ((¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴))))
11	7, 9, 10	e11 44708	. . . . . . . 8 ⊢ (   𝑥 ∈ 𝐴   ▶   ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴))   )
12	11	in1 44591	. . . . . . 7 ⊢ (𝑥 ∈ 𝐴 → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)))
13		idn1 44594	. . . . . . . . . . 11 ⊢ (   (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)   ▶   (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)   )
14		simpl 482	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) → 𝑥 ∈ 𝐵)
15	13, 14	e1a 44647	. . . . . . . . . 10 ⊢ (   (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)   ▶   𝑥 ∈ 𝐵   )
16		olc 869	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐵 → (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
17	15, 16	e1a 44647	. . . . . . . . 9 ⊢ (   (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)   ▶   (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)   )
18		simpr 484	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) → ¬ 𝑥 ∈ 𝐶)
19	13, 18	e1a 44647	. . . . . . . . . 10 ⊢ (   (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)   ▶    ¬ 𝑥 ∈ 𝐶   )
20		orc 868	. . . . . . . . . 10 ⊢ (¬ 𝑥 ∈ 𝐶 → (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴))
21	19, 20	e1a 44647	. . . . . . . . 9 ⊢ (   (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)   ▶   (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)   )
22	17, 21, 10	e11 44708	. . . . . . . 8 ⊢ (   (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)   ▶   ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴))   )
23	22	in1 44591	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)))
24	12, 23	jaoi 858	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)) → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)))
25		anddi 1013	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)) ↔ (((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶) ∨ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∨ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) ∨ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴))))
26	25	bicomi 224	. . . . . . 7 ⊢ ((((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶) ∨ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∨ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) ∨ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴))) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)))
27		idn1 44594	. . . . . . . . . . 11 ⊢ (   (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶)   ▶   (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶)   )
28		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶) → 𝑥 ∈ 𝐴)
29	28	orcd 874	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
30	27, 29	e1a 44647	. . . . . . . . . 10 ⊢ (   (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶)   ▶   (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶))   )
31	30	in1 44591	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
32		idn1 44594	. . . . . . . . . . . 12 ⊢ (   (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)   ▶   (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)   )
33		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
34	32, 33	e1a 44647	. . . . . . . . . . 11 ⊢ (   (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)   ▶   𝑥 ∈ 𝐴   )
35		orc 868	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
36	34, 35	e1a 44647	. . . . . . . . . 10 ⊢ (   (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)   ▶   (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶))   )
37	36	in1 44591	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
38	31, 37	jaoi 858	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶) ∨ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
39		olc 869	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
40	13, 39	e1a 44647	. . . . . . . . . 10 ⊢ (   (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)   ▶   (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶))   )
41	40	in1 44591	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
42		idn1 44594	. . . . . . . . . . . 12 ⊢ (   (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)   ▶   (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)   )
43		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
44	42, 43	e1a 44647	. . . . . . . . . . 11 ⊢ (   (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)   ▶   𝑥 ∈ 𝐴   )
45	44, 35	e1a 44647	. . . . . . . . . 10 ⊢ (   (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)   ▶   (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶))   )
46	45	in1 44591	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
47	41, 46	jaoi 858	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) ∨ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)) → (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
48	38, 47	jaoi 858	. . . . . . 7 ⊢ ((((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶) ∨ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∨ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶) ∨ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴))) → (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
49	26, 48	sylbir 235	. . . . . 6 ⊢ (((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)) → (𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
50	24, 49	impbii 209	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)))
51	4, 50	bitri 275	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∪ (𝐵 ∖ 𝐶)) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ (¬ 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴)))
52		eldif 3961	. . . . 5 ⊢ (𝑥 ∈ ((𝐴 ∪ 𝐵) ∖ (𝐶 ∖ 𝐴)) ↔ (𝑥 ∈ (𝐴 ∪ 𝐵) ∧ ¬ 𝑥 ∈ (𝐶 ∖ 𝐴)))
53		elun 4153	. . . . . 6 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
54		eldif 3961	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐶 ∖ 𝐴) ↔ (𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐴))
55	54	notbii 320	. . . . . . 7 ⊢ (¬ 𝑥 ∈ (𝐶 ∖ 𝐴) ↔ ¬ (𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐴))
56		pm4.53 988	. . . . . . 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 2730	. . 3 ⊢ ((𝐴 ∪ (𝐵 ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ (𝐶 ∖ 𝐴)) ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ (𝐵 ∖ 𝐶)) ↔ 𝑥 ∈ ((𝐴 ∪ 𝐵) ∖ (𝐶 ∖ 𝐴))))
63	62	biimpri 228	. 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ (𝐵 ∖ 𝐶)) ↔ 𝑥 ∈ ((𝐴 ∪ 𝐵) ∖ (𝐶 ∖ 𝐴))) → (𝐴 ∪ (𝐵 ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ (𝐶 ∖ 𝐴)))
64	61, 63	e0a 44792	1 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ (𝐶 ∖ 𝐴))

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954  df-un 3956  df-vd1 44590

This theorem is referenced by: (None)