| Step | Hyp | Ref
| Expression |
| 1 | | elex 3501 |
. . 3
⊢ (𝐵 ∈ dom 𝐴 → 𝐵 ∈ V) |
| 2 | 1 | anim2i 617 |
. 2
⊢ ((Rel
𝐴 ∧ 𝐵 ∈ dom 𝐴) → (Rel 𝐴 ∧ 𝐵 ∈ V)) |
| 3 | | id 22 |
. . . . 5
⊢
((1st ‘𝑥) = 𝐵 → (1st ‘𝑥) = 𝐵) |
| 4 | | fvex 6919 |
. . . . 5
⊢
(1st ‘𝑥) ∈ V |
| 5 | 3, 4 | eqeltrrdi 2850 |
. . . 4
⊢
((1st ‘𝑥) = 𝐵 → 𝐵 ∈ V) |
| 6 | 5 | rexlimivw 3151 |
. . 3
⊢
(∃𝑥 ∈
𝐴 (1st
‘𝑥) = 𝐵 → 𝐵 ∈ V) |
| 7 | 6 | anim2i 617 |
. 2
⊢ ((Rel
𝐴 ∧ ∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐵) → (Rel 𝐴 ∧ 𝐵 ∈ V)) |
| 8 | | eldm2g 5910 |
. . . 4
⊢ (𝐵 ∈ V → (𝐵 ∈ dom 𝐴 ↔ ∃𝑦〈𝐵, 𝑦〉 ∈ 𝐴)) |
| 9 | 8 | adantl 481 |
. . 3
⊢ ((Rel
𝐴 ∧ 𝐵 ∈ V) → (𝐵 ∈ dom 𝐴 ↔ ∃𝑦〈𝐵, 𝑦〉 ∈ 𝐴)) |
| 10 | | df-rel 5692 |
. . . . . . . . 9
⊢ (Rel
𝐴 ↔ 𝐴 ⊆ (V × V)) |
| 11 | | ssel 3977 |
. . . . . . . . 9
⊢ (𝐴 ⊆ (V × V) →
(𝑥 ∈ 𝐴 → 𝑥 ∈ (V × V))) |
| 12 | 10, 11 | sylbi 217 |
. . . . . . . 8
⊢ (Rel
𝐴 → (𝑥 ∈ 𝐴 → 𝑥 ∈ (V × V))) |
| 13 | 12 | imp 406 |
. . . . . . 7
⊢ ((Rel
𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ (V × V)) |
| 14 | | op1steq 8058 |
. . . . . . 7
⊢ (𝑥 ∈ (V × V) →
((1st ‘𝑥)
= 𝐵 ↔ ∃𝑦 𝑥 = 〈𝐵, 𝑦〉)) |
| 15 | 13, 14 | syl 17 |
. . . . . 6
⊢ ((Rel
𝐴 ∧ 𝑥 ∈ 𝐴) → ((1st ‘𝑥) = 𝐵 ↔ ∃𝑦 𝑥 = 〈𝐵, 𝑦〉)) |
| 16 | 15 | rexbidva 3177 |
. . . . 5
⊢ (Rel
𝐴 → (∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐵 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 𝑥 = 〈𝐵, 𝑦〉)) |
| 17 | 16 | adantr 480 |
. . . 4
⊢ ((Rel
𝐴 ∧ 𝐵 ∈ V) → (∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐵 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 𝑥 = 〈𝐵, 𝑦〉)) |
| 18 | | rexcom4 3288 |
. . . . 5
⊢
(∃𝑥 ∈
𝐴 ∃𝑦 𝑥 = 〈𝐵, 𝑦〉 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝑥 = 〈𝐵, 𝑦〉) |
| 19 | | risset 3233 |
. . . . . 6
⊢
(〈𝐵, 𝑦〉 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑥 = 〈𝐵, 𝑦〉) |
| 20 | 19 | exbii 1848 |
. . . . 5
⊢
(∃𝑦〈𝐵, 𝑦〉 ∈ 𝐴 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝑥 = 〈𝐵, 𝑦〉) |
| 21 | 18, 20 | bitr4i 278 |
. . . 4
⊢
(∃𝑥 ∈
𝐴 ∃𝑦 𝑥 = 〈𝐵, 𝑦〉 ↔ ∃𝑦〈𝐵, 𝑦〉 ∈ 𝐴) |
| 22 | 17, 21 | bitrdi 287 |
. . 3
⊢ ((Rel
𝐴 ∧ 𝐵 ∈ V) → (∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐵 ↔ ∃𝑦〈𝐵, 𝑦〉 ∈ 𝐴)) |
| 23 | 9, 22 | bitr4d 282 |
. 2
⊢ ((Rel
𝐴 ∧ 𝐵 ∈ V) → (𝐵 ∈ dom 𝐴 ↔ ∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐵)) |
| 24 | 2, 7, 23 | pm5.21nd 802 |
1
⊢ (Rel
𝐴 → (𝐵 ∈ dom 𝐴 ↔ ∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐵)) |