Proof of Theorem pm14.123b
Step | Hyp | Ref
| Expression |
1 | | 2sbc5g 42004 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑧∃𝑤((𝑧 = 𝐴 ∧ 𝑤 = 𝐵) ∧ 𝜑) ↔ [𝐴 / 𝑧][𝐵 / 𝑤]𝜑)) |
2 | 1 | adantr 481 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵))) → (∃𝑧∃𝑤((𝑧 = 𝐴 ∧ 𝑤 = 𝐵) ∧ 𝜑) ↔ [𝐴 / 𝑧][𝐵 / 𝑤]𝜑)) |
3 | | nfa1 2152 |
. . . . 5
⊢
Ⅎ𝑧∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) |
4 | | nfa2 2174 |
. . . . . 6
⊢
Ⅎ𝑤∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) |
5 | | simpr 485 |
. . . . . . 7
⊢ (((𝑧 = 𝐴 ∧ 𝑤 = 𝐵) ∧ 𝜑) → 𝜑) |
6 | | 2sp 2183 |
. . . . . . . 8
⊢
(∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) → (𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵))) |
7 | 6 | ancrd 552 |
. . . . . . 7
⊢
(∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) → (𝜑 → ((𝑧 = 𝐴 ∧ 𝑤 = 𝐵) ∧ 𝜑))) |
8 | 5, 7 | impbid2 225 |
. . . . . 6
⊢
(∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) → (((𝑧 = 𝐴 ∧ 𝑤 = 𝐵) ∧ 𝜑) ↔ 𝜑)) |
9 | 4, 8 | exbid 2220 |
. . . . 5
⊢
(∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) → (∃𝑤((𝑧 = 𝐴 ∧ 𝑤 = 𝐵) ∧ 𝜑) ↔ ∃𝑤𝜑)) |
10 | 3, 9 | exbid 2220 |
. . . 4
⊢
(∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) → (∃𝑧∃𝑤((𝑧 = 𝐴 ∧ 𝑤 = 𝐵) ∧ 𝜑) ↔ ∃𝑧∃𝑤𝜑)) |
11 | 10 | adantl 482 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵))) → (∃𝑧∃𝑤((𝑧 = 𝐴 ∧ 𝑤 = 𝐵) ∧ 𝜑) ↔ ∃𝑧∃𝑤𝜑)) |
12 | 2, 11 | bitr3d 280 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵))) → ([𝐴 / 𝑧][𝐵 / 𝑤]𝜑 ↔ ∃𝑧∃𝑤𝜑)) |
13 | 12 | pm5.32da 579 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ∧ [𝐴 / 𝑧][𝐵 / 𝑤]𝜑) ↔ (∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ∧ ∃𝑧∃𝑤𝜑))) |