Proof of Theorem bnj1468
| Step | Hyp | Ref
| Expression |
| 1 | | sbccow 3811 |
. 2
⊢
([𝐴 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑) |
| 2 | | ax-5 1910 |
. . 3
⊢ (𝜓 → ∀𝑦𝜓) |
| 3 | | bnj1468.3 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) |
| 4 | 3 | nfcii 2894 |
. . . . . . 7
⊢
Ⅎ𝑥𝐴 |
| 5 | 4 | nfeq2 2923 |
. . . . . 6
⊢
Ⅎ𝑥 𝑦 = 𝐴 |
| 6 | | nfsbc1v 3808 |
. . . . . . 7
⊢
Ⅎ𝑥[𝑦 / 𝑥]𝜑 |
| 7 | | bnj1468.1 |
. . . . . . . 8
⊢ (𝜓 → ∀𝑥𝜓) |
| 8 | 7 | nf5i 2146 |
. . . . . . 7
⊢
Ⅎ𝑥𝜓 |
| 9 | 6, 8 | nfbi 1903 |
. . . . . 6
⊢
Ⅎ𝑥([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
| 10 | 5, 9 | nfim 1896 |
. . . . 5
⊢
Ⅎ𝑥(𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ 𝜓)) |
| 11 | 10 | nf5ri 2195 |
. . . 4
⊢ ((𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ 𝜓)) → ∀𝑥(𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ 𝜓))) |
| 12 | | ax6ev 1969 |
. . . . 5
⊢
∃𝑥 𝑥 = 𝑦 |
| 13 | | eqeq1 2741 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 = 𝐴 ↔ 𝑦 = 𝐴)) |
| 14 | | bnj1468.2 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
| 15 | 13, 14 | biimtrrdi 254 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑦 = 𝐴 → (𝜑 ↔ 𝜓))) |
| 16 | | sbceq1a 3799 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑)) |
| 17 | 16 | bibi1d 343 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝜑 ↔ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ↔ 𝜓))) |
| 18 | 15, 17 | sylibd 239 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ 𝜓))) |
| 19 | 12, 18 | bnj101 34737 |
. . . 4
⊢
∃𝑥(𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ 𝜓)) |
| 20 | 11, 19 | bnj1131 34801 |
. . 3
⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ 𝜓)) |
| 21 | 2, 20 | bnj1464 34858 |
. 2
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑦][𝑦 / 𝑥]𝜑 ↔ 𝜓)) |
| 22 | 1, 21 | bitr3id 285 |
1
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓)) |