Proof of Theorem copsex2t
Step | Hyp | Ref
| Expression |
1 | | nfa1 2152 |
. . 3
⊢
Ⅎ𝑥∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) |
2 | | nfe1 2151 |
. . . 4
⊢
Ⅎ𝑥∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) |
3 | | nfv 1922 |
. . . 4
⊢
Ⅎ𝑥𝜓 |
4 | 2, 3 | nfbi 1911 |
. . 3
⊢
Ⅎ𝑥(∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ 𝜓) |
5 | | nfa2 2174 |
. . . 4
⊢
Ⅎ𝑦∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) |
6 | | nfe1 2151 |
. . . . . 6
⊢
Ⅎ𝑦∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) |
7 | 6 | nfex 2323 |
. . . . 5
⊢
Ⅎ𝑦∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) |
8 | | nfv 1922 |
. . . . 5
⊢
Ⅎ𝑦𝜓 |
9 | 7, 8 | nfbi 1911 |
. . . 4
⊢
Ⅎ𝑦(∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ 𝜓) |
10 | | opeq12 4786 |
. . . . . . . 8
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 〈𝑥, 𝑦〉 = 〈𝐴, 𝐵〉) |
11 | | copsexgw 5373 |
. . . . . . . . 9
⊢
(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 → (𝜑 ↔ ∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑))) |
12 | 11 | eqcoms 2745 |
. . . . . . . 8
⊢
(〈𝑥, 𝑦〉 = 〈𝐴, 𝐵〉 → (𝜑 ↔ ∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑))) |
13 | 10, 12 | syl 17 |
. . . . . . 7
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ ∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑))) |
14 | 13 | adantl 485 |
. . . . . 6
⊢
((∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜑 ↔ ∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑))) |
15 | | 2sp 2183 |
. . . . . . 7
⊢
(∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) → ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))) |
16 | 15 | imp 410 |
. . . . . 6
⊢
((∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜑 ↔ 𝜓)) |
17 | 14, 16 | bitr3d 284 |
. . . . 5
⊢
((∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ 𝜓)) |
18 | 17 | ex 416 |
. . . 4
⊢
(∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) → ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ 𝜓))) |
19 | 5, 9, 18 | exlimd 2216 |
. . 3
⊢
(∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) → (∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ 𝜓))) |
20 | 1, 4, 19 | exlimd 2216 |
. 2
⊢
(∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) → (∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ 𝜓))) |
21 | | elisset 2819 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) |
22 | | elisset 2819 |
. . . 4
⊢ (𝐵 ∈ 𝑊 → ∃𝑦 𝑦 = 𝐵) |
23 | 21, 22 | anim12i 616 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵)) |
24 | | exdistrv 1964 |
. . 3
⊢
(∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ↔ (∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵)) |
25 | 23, 24 | sylibr 237 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) |
26 | 20, 25 | impel 509 |
1
⊢
((∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ 𝜓)) |