Step | Hyp | Ref
| Expression |
1 | | noel 4264 |
. . . . . 6
⊢ ¬
𝑥 ∈
∅ |
2 | 1 | intnan 487 |
. . . . 5
⊢ ¬
(¬ (𝐴 ∈ V ∧
𝐵 ∈ V) ∧ 𝑥 ∈
∅) |
3 | | biorf 934 |
. . . . 5
⊢ (¬
(¬ (𝐴 ∈ V ∧
𝐵 ∈ V) ∧ 𝑥 ∈ ∅) → (((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}}) ↔ ((¬ (𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝑥 ∈ ∅) ∨ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})))) |
4 | 2, 3 | ax-mp 5 |
. . . 4
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}}) ↔ ((¬ (𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝑥 ∈ ∅) ∨ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}}))) |
5 | | df-3an 1088 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}}) ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})) |
6 | | orcom 867 |
. . . 4
⊢ ((((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}}) ∨ (¬ (𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝑥 ∈ ∅)) ↔ ((¬ (𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝑥 ∈ ∅) ∨ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}}))) |
7 | 4, 5, 6 | 3bitr4i 303 |
. . 3
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}}) ↔ (((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}}) ∨ (¬ (𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝑥 ∈ ∅))) |
8 | | eleq1 2826 |
. . . . . 6
⊢ (𝑦 = 𝑥 → (𝑦 ∈ {{𝐴}, {𝐴, 𝐵}} ↔ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})) |
9 | 8 | 3anbi3d 1441 |
. . . . 5
⊢ (𝑦 = 𝑥 → ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑦 ∈ {{𝐴}, {𝐴, 𝐵}}) ↔ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}}))) |
10 | | df-op 4568 |
. . . . 5
⊢
〈𝐴, 𝐵〉 = {𝑦 ∣ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑦 ∈ {{𝐴}, {𝐴, 𝐵}})} |
11 | 9, 10 | elab2g 3611 |
. . . 4
⊢ (𝑥 ∈ V → (𝑥 ∈ 〈𝐴, 𝐵〉 ↔ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}}))) |
12 | 11 | elv 3438 |
. . 3
⊢ (𝑥 ∈ 〈𝐴, 𝐵〉 ↔ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})) |
13 | | elif 4502 |
. . 3
⊢ (𝑥 ∈ if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅) ↔ (((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}}) ∨ (¬ (𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝑥 ∈ ∅))) |
14 | 7, 12, 13 | 3bitr4i 303 |
. 2
⊢ (𝑥 ∈ 〈𝐴, 𝐵〉 ↔ 𝑥 ∈ if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)) |
15 | 14 | eqriv 2735 |
1
⊢
〈𝐴, 𝐵〉 = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅) |