Proof of Theorem copsex2t
| Step | Hyp | Ref
| Expression |
| 1 | | nfa1 2151 |
. . 3
⊢
Ⅎ𝑥∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) |
| 2 | | nfe1 2150 |
. . . 4
⊢
Ⅎ𝑥∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) |
| 3 | | nfv 1914 |
. . . 4
⊢
Ⅎ𝑥𝜓 |
| 4 | 2, 3 | nfbi 1903 |
. . 3
⊢
Ⅎ𝑥(∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ 𝜓) |
| 5 | | nfa2 2176 |
. . . 4
⊢
Ⅎ𝑦∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) |
| 6 | | nfe1 2150 |
. . . . . 6
⊢
Ⅎ𝑦∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) |
| 7 | 6 | nfex 2324 |
. . . . 5
⊢
Ⅎ𝑦∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) |
| 8 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑦𝜓 |
| 9 | 7, 8 | nfbi 1903 |
. . . 4
⊢
Ⅎ𝑦(∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ 𝜓) |
| 10 | | opeq12 4875 |
. . . . . . . 8
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 〈𝑥, 𝑦〉 = 〈𝐴, 𝐵〉) |
| 11 | | copsexgw 5495 |
. . . . . . . . 9
⊢
(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 → (𝜑 ↔ ∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑))) |
| 12 | 11 | eqcoms 2745 |
. . . . . . . 8
⊢
(〈𝑥, 𝑦〉 = 〈𝐴, 𝐵〉 → (𝜑 ↔ ∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑))) |
| 13 | 10, 12 | syl 17 |
. . . . . . 7
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ ∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑))) |
| 14 | 13 | adantl 481 |
. . . . . 6
⊢
((∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜑 ↔ ∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑))) |
| 15 | | 2sp 2186 |
. . . . . . 7
⊢
(∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) → ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))) |
| 16 | 15 | imp 406 |
. . . . . 6
⊢
((∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜑 ↔ 𝜓)) |
| 17 | 14, 16 | bitr3d 281 |
. . . . 5
⊢
((∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ 𝜓)) |
| 18 | 17 | ex 412 |
. . . 4
⊢
(∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) → ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ 𝜓))) |
| 19 | 5, 9, 18 | exlimd 2218 |
. . 3
⊢
(∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) → (∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ 𝜓))) |
| 20 | 1, 4, 19 | exlimd 2218 |
. 2
⊢
(∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) → (∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ 𝜓))) |
| 21 | | elisset 2823 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) |
| 22 | | elisset 2823 |
. . . 4
⊢ (𝐵 ∈ 𝑊 → ∃𝑦 𝑦 = 𝐵) |
| 23 | 21, 22 | anim12i 613 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵)) |
| 24 | | exdistrv 1955 |
. . 3
⊢
(∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ↔ (∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵)) |
| 25 | 23, 24 | sylibr 234 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) |
| 26 | 20, 25 | impel 505 |
1
⊢
((∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ 𝜓)) |