Proof of Theorem bnj1468
Step | Hyp | Ref
| Expression |
1 | | sbccow 3739 |
. 2
⊢
([𝐴 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑) |
2 | | ax-5 1913 |
. . 3
⊢ (𝜓 → ∀𝑦𝜓) |
3 | | bnj1468.3 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) |
4 | 3 | nfcii 2891 |
. . . . . . 7
⊢
Ⅎ𝑥𝐴 |
5 | 4 | nfeq2 2924 |
. . . . . 6
⊢
Ⅎ𝑥 𝑦 = 𝐴 |
6 | | nfsbc1v 3736 |
. . . . . . 7
⊢
Ⅎ𝑥[𝑦 / 𝑥]𝜑 |
7 | | bnj1468.1 |
. . . . . . . 8
⊢ (𝜓 → ∀𝑥𝜓) |
8 | 7 | nf5i 2142 |
. . . . . . 7
⊢
Ⅎ𝑥𝜓 |
9 | 6, 8 | nfbi 1906 |
. . . . . 6
⊢
Ⅎ𝑥([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
10 | 5, 9 | nfim 1899 |
. . . . 5
⊢
Ⅎ𝑥(𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ 𝜓)) |
11 | 10 | nf5ri 2188 |
. . . 4
⊢ ((𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ 𝜓)) → ∀𝑥(𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ 𝜓))) |
12 | | ax6ev 1973 |
. . . . 5
⊢
∃𝑥 𝑥 = 𝑦 |
13 | | eqeq1 2742 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 = 𝐴 ↔ 𝑦 = 𝐴)) |
14 | | bnj1468.2 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
15 | 13, 14 | syl6bir 253 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑦 = 𝐴 → (𝜑 ↔ 𝜓))) |
16 | | sbceq1a 3727 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑)) |
17 | 16 | bibi1d 344 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝜑 ↔ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ↔ 𝜓))) |
18 | 15, 17 | sylibd 238 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ 𝜓))) |
19 | 12, 18 | bnj101 32702 |
. . . 4
⊢
∃𝑥(𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ 𝜓)) |
20 | 11, 19 | bnj1131 32767 |
. . 3
⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ 𝜓)) |
21 | 2, 20 | bnj1464 32824 |
. 2
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑦][𝑦 / 𝑥]𝜑 ↔ 𝜓)) |
22 | 1, 21 | bitr3id 285 |
1
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓)) |