Step | Hyp | Ref
| Expression |
1 | | reu3 3666 |
. 2
⊢
(∃!𝑝 ∈
(𝑋 × 𝑌)𝜓 ↔ (∃𝑝 ∈ (𝑋 × 𝑌)𝜓 ∧ ∃𝑞 ∈ (𝑋 × 𝑌)∀𝑝 ∈ (𝑋 × 𝑌)(𝜓 → 𝑝 = 𝑞))) |
2 | | reu3op.a |
. . . 4
⊢ (𝑝 = 〈𝑎, 𝑏〉 → (𝜓 ↔ 𝜒)) |
3 | 2 | rexxp 5750 |
. . 3
⊢
(∃𝑝 ∈
(𝑋 × 𝑌)𝜓 ↔ ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 𝜒) |
4 | | eqeq2 2752 |
. . . . . . 7
⊢ (𝑞 = 〈𝑥, 𝑦〉 → (𝑝 = 𝑞 ↔ 𝑝 = 〈𝑥, 𝑦〉)) |
5 | 4 | imbi2d 341 |
. . . . . 6
⊢ (𝑞 = 〈𝑥, 𝑦〉 → ((𝜓 → 𝑝 = 𝑞) ↔ (𝜓 → 𝑝 = 〈𝑥, 𝑦〉))) |
6 | 5 | ralbidv 3123 |
. . . . 5
⊢ (𝑞 = 〈𝑥, 𝑦〉 → (∀𝑝 ∈ (𝑋 × 𝑌)(𝜓 → 𝑝 = 𝑞) ↔ ∀𝑝 ∈ (𝑋 × 𝑌)(𝜓 → 𝑝 = 〈𝑥, 𝑦〉))) |
7 | 6 | rexxp 5750 |
. . . 4
⊢
(∃𝑞 ∈
(𝑋 × 𝑌)∀𝑝 ∈ (𝑋 × 𝑌)(𝜓 → 𝑝 = 𝑞) ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 ∀𝑝 ∈ (𝑋 × 𝑌)(𝜓 → 𝑝 = 〈𝑥, 𝑦〉)) |
8 | | eqeq1 2744 |
. . . . . . . 8
⊢ (𝑝 = 〈𝑎, 𝑏〉 → (𝑝 = 〈𝑥, 𝑦〉 ↔ 〈𝑎, 𝑏〉 = 〈𝑥, 𝑦〉)) |
9 | 2, 8 | imbi12d 345 |
. . . . . . 7
⊢ (𝑝 = 〈𝑎, 𝑏〉 → ((𝜓 → 𝑝 = 〈𝑥, 𝑦〉) ↔ (𝜒 → 〈𝑎, 𝑏〉 = 〈𝑥, 𝑦〉))) |
10 | 9 | ralxp 5749 |
. . . . . 6
⊢
(∀𝑝 ∈
(𝑋 × 𝑌)(𝜓 → 𝑝 = 〈𝑥, 𝑦〉) ↔ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑌 (𝜒 → 〈𝑎, 𝑏〉 = 〈𝑥, 𝑦〉)) |
11 | | eqcom 2747 |
. . . . . . . . 9
⊢
(〈𝑎, 𝑏〉 = 〈𝑥, 𝑦〉 ↔ 〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉) |
12 | 11 | a1i 11 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌)) → (〈𝑎, 𝑏〉 = 〈𝑥, 𝑦〉 ↔ 〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉)) |
13 | 12 | imbi2d 341 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌)) → ((𝜒 → 〈𝑎, 𝑏〉 = 〈𝑥, 𝑦〉) ↔ (𝜒 → 〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉))) |
14 | 13 | 2ralbidva 3124 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → (∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑌 (𝜒 → 〈𝑎, 𝑏〉 = 〈𝑥, 𝑦〉) ↔ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑌 (𝜒 → 〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉))) |
15 | 10, 14 | bitrid 282 |
. . . . 5
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → (∀𝑝 ∈ (𝑋 × 𝑌)(𝜓 → 𝑝 = 〈𝑥, 𝑦〉) ↔ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑌 (𝜒 → 〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉))) |
16 | 15 | 2rexbiia 3229 |
. . . 4
⊢
(∃𝑥 ∈
𝑋 ∃𝑦 ∈ 𝑌 ∀𝑝 ∈ (𝑋 × 𝑌)(𝜓 → 𝑝 = 〈𝑥, 𝑦〉) ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑌 (𝜒 → 〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉)) |
17 | 7, 16 | bitri 274 |
. . 3
⊢
(∃𝑞 ∈
(𝑋 × 𝑌)∀𝑝 ∈ (𝑋 × 𝑌)(𝜓 → 𝑝 = 𝑞) ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑌 (𝜒 → 〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉)) |
18 | 3, 17 | anbi12i 627 |
. 2
⊢
((∃𝑝 ∈
(𝑋 × 𝑌)𝜓 ∧ ∃𝑞 ∈ (𝑋 × 𝑌)∀𝑝 ∈ (𝑋 × 𝑌)(𝜓 → 𝑝 = 𝑞)) ↔ (∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 𝜒 ∧ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑌 (𝜒 → 〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉))) |
19 | 1, 18 | bitri 274 |
1
⊢
(∃!𝑝 ∈
(𝑋 × 𝑌)𝜓 ↔ (∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 𝜒 ∧ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑌 (𝜒 → 〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉))) |