| 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
⊢ (𝐴 ∪ (𝐵 ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ (𝐶 ∖ 𝐴)) |