Step | Hyp | Ref
| Expression |
1 | | csbeq1 3896 |
. . . 4
⊢ (𝑤 = 𝐴 → ⦋𝑤 / 𝑥⦌{⟨𝑦, 𝑧⟩ ∣ 𝜑} = ⦋𝐴 / 𝑥⦌{⟨𝑦, 𝑧⟩ ∣ 𝜑}) |
2 | | dfsbcq2 3780 |
. . . . 5
⊢ (𝑤 = 𝐴 → ([𝑤 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) |
3 | 2 | opabbidv 5214 |
. . . 4
⊢ (𝑤 = 𝐴 → {⟨𝑦, 𝑧⟩ ∣ [𝑤 / 𝑥]𝜑} = {⟨𝑦, 𝑧⟩ ∣ [𝐴 / 𝑥]𝜑}) |
4 | 1, 3 | eqeq12d 2748 |
. . 3
⊢ (𝑤 = 𝐴 → (⦋𝑤 / 𝑥⦌{⟨𝑦, 𝑧⟩ ∣ 𝜑} = {⟨𝑦, 𝑧⟩ ∣ [𝑤 / 𝑥]𝜑} ↔ ⦋𝐴 / 𝑥⦌{⟨𝑦, 𝑧⟩ ∣ 𝜑} = {⟨𝑦, 𝑧⟩ ∣ [𝐴 / 𝑥]𝜑})) |
5 | | vex 3478 |
. . . 4
⊢ 𝑤 ∈ V |
6 | | nfs1v 2153 |
. . . . 5
⊢
Ⅎ𝑥[𝑤 / 𝑥]𝜑 |
7 | 6 | nfopab 5217 |
. . . 4
⊢
Ⅎ𝑥{⟨𝑦, 𝑧⟩ ∣ [𝑤 / 𝑥]𝜑} |
8 | | sbequ12 2243 |
. . . . 5
⊢ (𝑥 = 𝑤 → (𝜑 ↔ [𝑤 / 𝑥]𝜑)) |
9 | 8 | opabbidv 5214 |
. . . 4
⊢ (𝑥 = 𝑤 → {⟨𝑦, 𝑧⟩ ∣ 𝜑} = {⟨𝑦, 𝑧⟩ ∣ [𝑤 / 𝑥]𝜑}) |
10 | 5, 7, 9 | csbief 3928 |
. . 3
⊢
⦋𝑤 /
𝑥⦌{⟨𝑦, 𝑧⟩ ∣ 𝜑} = {⟨𝑦, 𝑧⟩ ∣ [𝑤 / 𝑥]𝜑} |
11 | 4, 10 | vtoclg 3556 |
. 2
⊢ (𝐴 ∈ V →
⦋𝐴 / 𝑥⦌{⟨𝑦, 𝑧⟩ ∣ 𝜑} = {⟨𝑦, 𝑧⟩ ∣ [𝐴 / 𝑥]𝜑}) |
12 | | csbprc 4406 |
. . 3
⊢ (¬
𝐴 ∈ V →
⦋𝐴 / 𝑥⦌{⟨𝑦, 𝑧⟩ ∣ 𝜑} = ∅) |
13 | | sbcex 3787 |
. . . . . . 7
⊢
([𝐴 / 𝑥]𝜑 → 𝐴 ∈ V) |
14 | 13 | con3i 154 |
. . . . . 6
⊢ (¬
𝐴 ∈ V → ¬
[𝐴 / 𝑥]𝜑) |
15 | 14 | nexdv 1939 |
. . . . 5
⊢ (¬
𝐴 ∈ V → ¬
∃𝑧[𝐴 / 𝑥]𝜑) |
16 | 15 | nexdv 1939 |
. . . 4
⊢ (¬
𝐴 ∈ V → ¬
∃𝑦∃𝑧[𝐴 / 𝑥]𝜑) |
17 | | opabn0 5553 |
. . . . 5
⊢
({⟨𝑦, 𝑧⟩ ∣ [𝐴 / 𝑥]𝜑} ≠ ∅ ↔ ∃𝑦∃𝑧[𝐴 / 𝑥]𝜑) |
18 | 17 | necon1bbii 2990 |
. . . 4
⊢ (¬
∃𝑦∃𝑧[𝐴 / 𝑥]𝜑 ↔ {⟨𝑦, 𝑧⟩ ∣ [𝐴 / 𝑥]𝜑} = ∅) |
19 | 16, 18 | sylib 217 |
. . 3
⊢ (¬
𝐴 ∈ V →
{⟨𝑦, 𝑧⟩ ∣ [𝐴 / 𝑥]𝜑} = ∅) |
20 | 12, 19 | eqtr4d 2775 |
. 2
⊢ (¬
𝐴 ∈ V →
⦋𝐴 / 𝑥⦌{⟨𝑦, 𝑧⟩ ∣ 𝜑} = {⟨𝑦, 𝑧⟩ ∣ [𝐴 / 𝑥]𝜑}) |
21 | 11, 20 | pm2.61i 182 |
1
⊢
⦋𝐴 /
𝑥⦌{⟨𝑦, 𝑧⟩ ∣ 𝜑} = {⟨𝑦, 𝑧⟩ ∣ [𝐴 / 𝑥]𝜑} |