Step | Hyp | Ref
| Expression |
1 | | rexopabb.o |
. . 3
⊢ 𝑂 = {⟨𝑥, 𝑦⟩ ∣ 𝜑} |
2 | 1 | rexeqi 3359 |
. 2
⊢
(∃𝑜 ∈
𝑂 𝜓 ↔ ∃𝑜 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}𝜓) |
3 | | elopab 5453 |
. . . . 5
⊢ (𝑜 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥∃𝑦(𝑜 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) |
4 | | simprr 771 |
. . . . . . . . 9
⊢ ((𝜓 ∧ (𝑜 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) → 𝜑) |
5 | | rexopabb.p |
. . . . . . . . . . . 12
⊢ (𝑜 = ⟨𝑥, 𝑦⟩ → (𝜓 ↔ 𝜒)) |
6 | 5 | biimpd 228 |
. . . . . . . . . . 11
⊢ (𝑜 = ⟨𝑥, 𝑦⟩ → (𝜓 → 𝜒)) |
7 | 6 | adantr 482 |
. . . . . . . . . 10
⊢ ((𝑜 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → (𝜓 → 𝜒)) |
8 | 7 | impcom 409 |
. . . . . . . . 9
⊢ ((𝜓 ∧ (𝑜 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) → 𝜒) |
9 | 4, 8 | jca 513 |
. . . . . . . 8
⊢ ((𝜓 ∧ (𝑜 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) → (𝜑 ∧ 𝜒)) |
10 | 9 | ex 414 |
. . . . . . 7
⊢ (𝜓 → ((𝑜 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → (𝜑 ∧ 𝜒))) |
11 | 10 | 2eximdv 1920 |
. . . . . 6
⊢ (𝜓 → (∃𝑥∃𝑦(𝑜 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → ∃𝑥∃𝑦(𝜑 ∧ 𝜒))) |
12 | 11 | impcom 409 |
. . . . 5
⊢
((∃𝑥∃𝑦(𝑜 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ∧ 𝜓) → ∃𝑥∃𝑦(𝜑 ∧ 𝜒)) |
13 | 3, 12 | sylanb 582 |
. . . 4
⊢ ((𝑜 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ∧ 𝜓) → ∃𝑥∃𝑦(𝜑 ∧ 𝜒)) |
14 | 13 | rexlimiva 3141 |
. . 3
⊢
(∃𝑜 ∈
{⟨𝑥, 𝑦⟩ ∣ 𝜑}𝜓 → ∃𝑥∃𝑦(𝜑 ∧ 𝜒)) |
15 | | nfopab1 5151 |
. . . . 5
⊢
Ⅎ𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑} |
16 | | nfv 1915 |
. . . . 5
⊢
Ⅎ𝑥𝜓 |
17 | 15, 16 | nfrex 3301 |
. . . 4
⊢
Ⅎ𝑥∃𝑜 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}𝜓 |
18 | | nfopab2 5152 |
. . . . . 6
⊢
Ⅎ𝑦{⟨𝑥, 𝑦⟩ ∣ 𝜑} |
19 | | nfv 1915 |
. . . . . 6
⊢
Ⅎ𝑦𝜓 |
20 | 18, 19 | nfrex 3301 |
. . . . 5
⊢
Ⅎ𝑦∃𝑜 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}𝜓 |
21 | | opabidw 5450 |
. . . . . 6
⊢
(⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜑) |
22 | | opex 5392 |
. . . . . . 7
⊢
⟨𝑥, 𝑦⟩ ∈ V |
23 | 22, 5 | sbcie 3764 |
. . . . . 6
⊢
([⟨𝑥,
𝑦⟩ / 𝑜]𝜓 ↔ 𝜒) |
24 | | rspesbca 3819 |
. . . . . 6
⊢
((⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ∧ [⟨𝑥, 𝑦⟩ / 𝑜]𝜓) → ∃𝑜 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}𝜓) |
25 | 21, 23, 24 | syl2anbr 600 |
. . . . 5
⊢ ((𝜑 ∧ 𝜒) → ∃𝑜 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}𝜓) |
26 | 20, 25 | exlimi 2208 |
. . . 4
⊢
(∃𝑦(𝜑 ∧ 𝜒) → ∃𝑜 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}𝜓) |
27 | 17, 26 | exlimi 2208 |
. . 3
⊢
(∃𝑥∃𝑦(𝜑 ∧ 𝜒) → ∃𝑜 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}𝜓) |
28 | 14, 27 | impbii 208 |
. 2
⊢
(∃𝑜 ∈
{⟨𝑥, 𝑦⟩ ∣ 𝜑}𝜓 ↔ ∃𝑥∃𝑦(𝜑 ∧ 𝜒)) |
29 | 2, 28 | bitri 275 |
1
⊢
(∃𝑜 ∈
𝑂 𝜓 ↔ ∃𝑥∃𝑦(𝜑 ∧ 𝜒)) |