Step | Hyp | Ref
| Expression |
1 | | eqeq1 2742 |
. . . . . . 7
⊢ ({𝑥 ∣ 𝜑} = {𝑤} → ({𝑥 ∣ 𝜑} = {𝑧} ↔ {𝑤} = {𝑧})) |
2 | | sneqbg 4776 |
. . . . . . . . 9
⊢ (𝑤 ∈ V → ({𝑤} = {𝑧} ↔ 𝑤 = 𝑧)) |
3 | 2 | elv 3437 |
. . . . . . . 8
⊢ ({𝑤} = {𝑧} ↔ 𝑤 = 𝑧) |
4 | | equcom 2021 |
. . . . . . . 8
⊢ (𝑤 = 𝑧 ↔ 𝑧 = 𝑤) |
5 | 3, 4 | bitri 274 |
. . . . . . 7
⊢ ({𝑤} = {𝑧} ↔ 𝑧 = 𝑤) |
6 | 1, 5 | bitrdi 287 |
. . . . . 6
⊢ ({𝑥 ∣ 𝜑} = {𝑤} → ({𝑥 ∣ 𝜑} = {𝑧} ↔ 𝑧 = 𝑤)) |
7 | | sneq 4573 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → {𝑦} = {𝑧}) |
8 | 7 | eqeq2d 2749 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → ({𝑥 ∣ 𝜑} = {𝑦} ↔ {𝑥 ∣ 𝜑} = {𝑧})) |
9 | 8 | elabg 3608 |
. . . . . . 7
⊢ (𝑧 ∈ V → (𝑧 ∈ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} ↔ {𝑥 ∣ 𝜑} = {𝑧})) |
10 | 9 | elv 3437 |
. . . . . 6
⊢ (𝑧 ∈ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} ↔ {𝑥 ∣ 𝜑} = {𝑧}) |
11 | | velsn 4579 |
. . . . . 6
⊢ (𝑧 ∈ {𝑤} ↔ 𝑧 = 𝑤) |
12 | 6, 10, 11 | 3bitr4g 314 |
. . . . 5
⊢ ({𝑥 ∣ 𝜑} = {𝑤} → (𝑧 ∈ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} ↔ 𝑧 ∈ {𝑤})) |
13 | 12 | eqrdv 2736 |
. . . 4
⊢ ({𝑥 ∣ 𝜑} = {𝑤} → {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = {𝑤}) |
14 | | vsnid 4600 |
. . . . . 6
⊢ 𝑤 ∈ {𝑤} |
15 | | eleq2 2827 |
. . . . . 6
⊢ ({𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = {𝑤} → (𝑤 ∈ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} ↔ 𝑤 ∈ {𝑤})) |
16 | 14, 15 | mpbiri 257 |
. . . . 5
⊢ ({𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = {𝑤} → 𝑤 ∈ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}}) |
17 | | sneq 4573 |
. . . . . . . 8
⊢ (𝑦 = 𝑤 → {𝑦} = {𝑤}) |
18 | 17 | eqeq2d 2749 |
. . . . . . 7
⊢ (𝑦 = 𝑤 → ({𝑥 ∣ 𝜑} = {𝑦} ↔ {𝑥 ∣ 𝜑} = {𝑤})) |
19 | 18 | elabg 3608 |
. . . . . 6
⊢ (𝑤 ∈ V → (𝑤 ∈ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} ↔ {𝑥 ∣ 𝜑} = {𝑤})) |
20 | 19 | elv 3437 |
. . . . 5
⊢ (𝑤 ∈ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} ↔ {𝑥 ∣ 𝜑} = {𝑤}) |
21 | 16, 20 | sylib 217 |
. . . 4
⊢ ({𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = {𝑤} → {𝑥 ∣ 𝜑} = {𝑤}) |
22 | 13, 21 | impbii 208 |
. . 3
⊢ ({𝑥 ∣ 𝜑} = {𝑤} ↔ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = {𝑤}) |
23 | | sneq 4573 |
. . . . . 6
⊢ (𝑧 = 𝑤 → {𝑧} = {𝑤}) |
24 | 23 | eqeq2d 2749 |
. . . . 5
⊢ (𝑧 = 𝑤 → ({𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = {𝑧} ↔ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = {𝑤})) |
25 | 24 | elabg 3608 |
. . . 4
⊢ (𝑤 ∈ V → (𝑤 ∈ {𝑧 ∣ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = {𝑧}} ↔ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = {𝑤})) |
26 | 25 | elv 3437 |
. . 3
⊢ (𝑤 ∈ {𝑧 ∣ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = {𝑧}} ↔ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = {𝑤}) |
27 | 22, 20, 26 | 3bitr4i 303 |
. 2
⊢ (𝑤 ∈ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} ↔ 𝑤 ∈ {𝑧 ∣ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = {𝑧}}) |
28 | 27 | eqriv 2735 |
1
⊢ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = {𝑧 ∣ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = {𝑧}} |