| Step | Hyp | Ref
| Expression |
| 1 | | ssel 3977 |
. . . . . . 7
⊢ (𝐴 ⊆ 𝐶 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)) |
| 2 | | ssel 3977 |
. . . . . . 7
⊢ (𝐵 ⊆ 𝐶 → (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)) |
| 3 | | pm5.1 824 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)) → ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))) |
| 4 | 1, 2, 3 | syl2an 596 |
. . . . . 6
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))) |
| 5 | | con2b 359 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 → ¬ 𝑥 ∈ 𝐴)) |
| 6 | 5 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 → ¬ 𝑥 ∈ 𝐴))) |
| 7 | 4, 6 | anbi12d 632 |
. . . . 5
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → (((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵)) ↔ ((𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → ¬ 𝑥 ∈ 𝐴)))) |
| 8 | | jcab 517 |
. . . . 5
⊢ ((𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐵)) ↔ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))) |
| 9 | | jcab 517 |
. . . . 5
⊢ ((𝑥 ∈ 𝐵 → (𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐴)) ↔ ((𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → ¬ 𝑥 ∈ 𝐴))) |
| 10 | 7, 8, 9 | 3bitr4g 314 |
. . . 4
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → ((𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐵)) ↔ (𝑥 ∈ 𝐵 → (𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐴)))) |
| 11 | | eldif 3961 |
. . . . 5
⊢ (𝑥 ∈ (𝐶 ∖ 𝐵) ↔ (𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐵)) |
| 12 | 11 | imbi2i 336 |
. . . 4
⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐶 ∖ 𝐵)) ↔ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐵))) |
| 13 | | eldif 3961 |
. . . . 5
⊢ (𝑥 ∈ (𝐶 ∖ 𝐴) ↔ (𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐴)) |
| 14 | 13 | imbi2i 336 |
. . . 4
⊢ ((𝑥 ∈ 𝐵 → 𝑥 ∈ (𝐶 ∖ 𝐴)) ↔ (𝑥 ∈ 𝐵 → (𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐴))) |
| 15 | 10, 12, 14 | 3bitr4g 314 |
. . 3
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → ((𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐶 ∖ 𝐵)) ↔ (𝑥 ∈ 𝐵 → 𝑥 ∈ (𝐶 ∖ 𝐴)))) |
| 16 | 15 | albidv 1920 |
. 2
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐶 ∖ 𝐵)) ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ (𝐶 ∖ 𝐴)))) |
| 17 | | df-ss 3968 |
. 2
⊢ (𝐴 ⊆ (𝐶 ∖ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐶 ∖ 𝐵))) |
| 18 | | df-ss 3968 |
. 2
⊢ (𝐵 ⊆ (𝐶 ∖ 𝐴) ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ (𝐶 ∖ 𝐴))) |
| 19 | 16, 17, 18 | 3bitr4g 314 |
1
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → (𝐴 ⊆ (𝐶 ∖ 𝐵) ↔ 𝐵 ⊆ (𝐶 ∖ 𝐴))) |