Step | Hyp | Ref
| Expression |
1 | | reu3 3685 |
. 2
⊢
(∃!𝑝 ∈
(𝑋 × 𝑌)𝜓 ↔ (∃𝑝 ∈ (𝑋 × 𝑌)𝜓 ∧ ∃𝑞 ∈ (𝑋 × 𝑌)∀𝑝 ∈ (𝑋 × 𝑌)(𝜓 → 𝑝 = 𝑞))) |
2 | | reu3op.a |
. . . 4
⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜓 ↔ 𝜒)) |
3 | 2 | rexxp 5798 |
. . 3
⊢
(∃𝑝 ∈
(𝑋 × 𝑌)𝜓 ↔ ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 𝜒) |
4 | | eqeq2 2748 |
. . . . . . 7
⊢ (𝑞 = ⟨𝑥, 𝑦⟩ → (𝑝 = 𝑞 ↔ 𝑝 = ⟨𝑥, 𝑦⟩)) |
5 | 4 | imbi2d 340 |
. . . . . 6
⊢ (𝑞 = ⟨𝑥, 𝑦⟩ → ((𝜓 → 𝑝 = 𝑞) ↔ (𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩))) |
6 | 5 | ralbidv 3174 |
. . . . 5
⊢ (𝑞 = ⟨𝑥, 𝑦⟩ → (∀𝑝 ∈ (𝑋 × 𝑌)(𝜓 → 𝑝 = 𝑞) ↔ ∀𝑝 ∈ (𝑋 × 𝑌)(𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩))) |
7 | 6 | rexxp 5798 |
. . . 4
⊢
(∃𝑞 ∈
(𝑋 × 𝑌)∀𝑝 ∈ (𝑋 × 𝑌)(𝜓 → 𝑝 = 𝑞) ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 ∀𝑝 ∈ (𝑋 × 𝑌)(𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩)) |
8 | | eqeq1 2740 |
. . . . . . . 8
⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (𝑝 = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑎, 𝑏⟩ = ⟨𝑥, 𝑦⟩)) |
9 | 2, 8 | imbi12d 344 |
. . . . . . 7
⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → ((𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩) ↔ (𝜒 → ⟨𝑎, 𝑏⟩ = ⟨𝑥, 𝑦⟩))) |
10 | 9 | ralxp 5797 |
. . . . . 6
⊢
(∀𝑝 ∈
(𝑋 × 𝑌)(𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩) ↔ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑌 (𝜒 → ⟨𝑎, 𝑏⟩ = ⟨𝑥, 𝑦⟩)) |
11 | | eqcom 2743 |
. . . . . . . . 9
⊢
(⟨𝑎, 𝑏⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩) |
12 | 11 | a1i 11 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌)) → (⟨𝑎, 𝑏⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)) |
13 | 12 | imbi2d 340 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌)) → ((𝜒 → ⟨𝑎, 𝑏⟩ = ⟨𝑥, 𝑦⟩) ↔ (𝜒 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) |
14 | 13 | 2ralbidva 3210 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → (∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑌 (𝜒 → ⟨𝑎, 𝑏⟩ = ⟨𝑥, 𝑦⟩) ↔ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑌 (𝜒 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) |
15 | 10, 14 | bitrid 282 |
. . . . 5
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → (∀𝑝 ∈ (𝑋 × 𝑌)(𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩) ↔ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑌 (𝜒 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) |
16 | 15 | 2rexbiia 3209 |
. . . 4
⊢
(∃𝑥 ∈
𝑋 ∃𝑦 ∈ 𝑌 ∀𝑝 ∈ (𝑋 × 𝑌)(𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩) ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑌 (𝜒 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)) |
17 | 7, 16 | bitri 274 |
. . 3
⊢
(∃𝑞 ∈
(𝑋 × 𝑌)∀𝑝 ∈ (𝑋 × 𝑌)(𝜓 → 𝑝 = 𝑞) ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑌 (𝜒 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)) |
18 | 3, 17 | anbi12i 627 |
. 2
⊢
((∃𝑝 ∈
(𝑋 × 𝑌)𝜓 ∧ ∃𝑞 ∈ (𝑋 × 𝑌)∀𝑝 ∈ (𝑋 × 𝑌)(𝜓 → 𝑝 = 𝑞)) ↔ (∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 𝜒 ∧ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑌 (𝜒 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) |
19 | 1, 18 | bitri 274 |
1
⊢
(∃!𝑝 ∈
(𝑋 × 𝑌)𝜓 ↔ (∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 𝜒 ∧ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑌 (𝜒 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) |