Step | Hyp | Ref
| Expression |
1 | | sbcex2 3760 |
. . 3
⊢
([𝑍 / 𝑦]∃𝑤∀𝑥(𝜑 ↔ 𝑥 = 𝑤) ↔ ∃𝑤[𝑍 / 𝑦]∀𝑥(𝜑 ↔ 𝑥 = 𝑤)) |
2 | | sbcal 3759 |
. . . 4
⊢
([𝑍 / 𝑦]∀𝑥(𝜑 ↔ 𝑥 = 𝑤) ↔ ∀𝑥[𝑍 / 𝑦](𝜑 ↔ 𝑥 = 𝑤)) |
3 | 2 | exbii 1855 |
. . 3
⊢
(∃𝑤[𝑍 / 𝑦]∀𝑥(𝜑 ↔ 𝑥 = 𝑤) ↔ ∃𝑤∀𝑥[𝑍 / 𝑦](𝜑 ↔ 𝑥 = 𝑤)) |
4 | | bnj89.1 |
. . . . . . 7
⊢ 𝑍 ∈ V |
5 | | sbcbig 3748 |
. . . . . . 7
⊢ (𝑍 ∈ V → ([𝑍 / 𝑦](𝜑 ↔ 𝑥 = 𝑤) ↔ ([𝑍 / 𝑦]𝜑 ↔ [𝑍 / 𝑦]𝑥 = 𝑤))) |
6 | 4, 5 | ax-mp 5 |
. . . . . 6
⊢
([𝑍 / 𝑦](𝜑 ↔ 𝑥 = 𝑤) ↔ ([𝑍 / 𝑦]𝜑 ↔ [𝑍 / 𝑦]𝑥 = 𝑤)) |
7 | | sbcg 3774 |
. . . . . . . 8
⊢ (𝑍 ∈ V → ([𝑍 / 𝑦]𝑥 = 𝑤 ↔ 𝑥 = 𝑤)) |
8 | 4, 7 | ax-mp 5 |
. . . . . . 7
⊢
([𝑍 / 𝑦]𝑥 = 𝑤 ↔ 𝑥 = 𝑤) |
9 | 8 | bibi2i 341 |
. . . . . 6
⊢
(([𝑍 / 𝑦]𝜑 ↔ [𝑍 / 𝑦]𝑥 = 𝑤) ↔ ([𝑍 / 𝑦]𝜑 ↔ 𝑥 = 𝑤)) |
10 | 6, 9 | bitri 278 |
. . . . 5
⊢
([𝑍 / 𝑦](𝜑 ↔ 𝑥 = 𝑤) ↔ ([𝑍 / 𝑦]𝜑 ↔ 𝑥 = 𝑤)) |
11 | 10 | albii 1827 |
. . . 4
⊢
(∀𝑥[𝑍 / 𝑦](𝜑 ↔ 𝑥 = 𝑤) ↔ ∀𝑥([𝑍 / 𝑦]𝜑 ↔ 𝑥 = 𝑤)) |
12 | 11 | exbii 1855 |
. . 3
⊢
(∃𝑤∀𝑥[𝑍 / 𝑦](𝜑 ↔ 𝑥 = 𝑤) ↔ ∃𝑤∀𝑥([𝑍 / 𝑦]𝜑 ↔ 𝑥 = 𝑤)) |
13 | 1, 3, 12 | 3bitri 300 |
. 2
⊢
([𝑍 / 𝑦]∃𝑤∀𝑥(𝜑 ↔ 𝑥 = 𝑤) ↔ ∃𝑤∀𝑥([𝑍 / 𝑦]𝜑 ↔ 𝑥 = 𝑤)) |
14 | | eu6 2573 |
. . 3
⊢
(∃!𝑥𝜑 ↔ ∃𝑤∀𝑥(𝜑 ↔ 𝑥 = 𝑤)) |
15 | 14 | sbcbii 3755 |
. 2
⊢
([𝑍 / 𝑦]∃!𝑥𝜑 ↔ [𝑍 / 𝑦]∃𝑤∀𝑥(𝜑 ↔ 𝑥 = 𝑤)) |
16 | | eu6 2573 |
. 2
⊢
(∃!𝑥[𝑍 / 𝑦]𝜑 ↔ ∃𝑤∀𝑥([𝑍 / 𝑦]𝜑 ↔ 𝑥 = 𝑤)) |
17 | 13, 15, 16 | 3bitr4i 306 |
1
⊢
([𝑍 / 𝑦]∃!𝑥𝜑 ↔ ∃!𝑥[𝑍 / 𝑦]𝜑) |