Proof of Theorem bnj1468
Step | Hyp | Ref
| Expression |
1 | | sbccow 3702 |
. 2
⊢
([𝐴 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑) |
2 | | ax-5 1916 |
. . 3
⊢ (𝜓 → ∀𝑦𝜓) |
3 | | bnj1468.3 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) |
4 | 3 | nfcii 2883 |
. . . . . . 7
⊢
Ⅎ𝑥𝐴 |
5 | 4 | nfeq2 2916 |
. . . . . 6
⊢
Ⅎ𝑥 𝑦 = 𝐴 |
6 | | nfsbc1v 3699 |
. . . . . . 7
⊢
Ⅎ𝑥[𝑦 / 𝑥]𝜑 |
7 | | bnj1468.1 |
. . . . . . . 8
⊢ (𝜓 → ∀𝑥𝜓) |
8 | 7 | nf5i 2149 |
. . . . . . 7
⊢
Ⅎ𝑥𝜓 |
9 | 6, 8 | nfbi 1909 |
. . . . . 6
⊢
Ⅎ𝑥([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
10 | 5, 9 | nfim 1902 |
. . . . 5
⊢
Ⅎ𝑥(𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ 𝜓)) |
11 | 10 | nf5ri 2196 |
. . . 4
⊢ ((𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ 𝜓)) → ∀𝑥(𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ 𝜓))) |
12 | | ax6ev 1976 |
. . . . 5
⊢
∃𝑥 𝑥 = 𝑦 |
13 | | eqeq1 2742 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 = 𝐴 ↔ 𝑦 = 𝐴)) |
14 | | bnj1468.2 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
15 | 13, 14 | syl6bir 257 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑦 = 𝐴 → (𝜑 ↔ 𝜓))) |
16 | | sbceq1a 3690 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑)) |
17 | 16 | bibi1d 347 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝜑 ↔ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ↔ 𝜓))) |
18 | 15, 17 | sylibd 242 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ 𝜓))) |
19 | 12, 18 | bnj101 32264 |
. . . 4
⊢
∃𝑥(𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ 𝜓)) |
20 | 11, 19 | bnj1131 32330 |
. . 3
⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ 𝜓)) |
21 | 2, 20 | bnj1464 32387 |
. 2
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑦][𝑦 / 𝑥]𝜑 ↔ 𝜓)) |
22 | 1, 21 | bitr3id 288 |
1
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓)) |