Step | Hyp | Ref
| Expression |
1 | | elex 3464 |
. . 3
⊢ (𝐵 ∈ dom 𝐴 → 𝐵 ∈ V) |
2 | 1 | anim2i 618 |
. 2
⊢ ((Rel
𝐴 ∧ 𝐵 ∈ dom 𝐴) → (Rel 𝐴 ∧ 𝐵 ∈ V)) |
3 | | id 22 |
. . . . 5
⊢
((1st ‘𝑥) = 𝐵 → (1st ‘𝑥) = 𝐵) |
4 | | fvex 6856 |
. . . . 5
⊢
(1st ‘𝑥) ∈ V |
5 | 3, 4 | eqeltrrdi 2847 |
. . . 4
⊢
((1st ‘𝑥) = 𝐵 → 𝐵 ∈ V) |
6 | 5 | rexlimivw 3149 |
. . 3
⊢
(∃𝑥 ∈
𝐴 (1st
‘𝑥) = 𝐵 → 𝐵 ∈ V) |
7 | 6 | anim2i 618 |
. 2
⊢ ((Rel
𝐴 ∧ ∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐵) → (Rel 𝐴 ∧ 𝐵 ∈ V)) |
8 | | eldm2g 5856 |
. . . 4
⊢ (𝐵 ∈ V → (𝐵 ∈ dom 𝐴 ↔ ∃𝑦⟨𝐵, 𝑦⟩ ∈ 𝐴)) |
9 | 8 | adantl 483 |
. . 3
⊢ ((Rel
𝐴 ∧ 𝐵 ∈ V) → (𝐵 ∈ dom 𝐴 ↔ ∃𝑦⟨𝐵, 𝑦⟩ ∈ 𝐴)) |
10 | | df-rel 5641 |
. . . . . . . . 9
⊢ (Rel
𝐴 ↔ 𝐴 ⊆ (V × V)) |
11 | | ssel 3938 |
. . . . . . . . 9
⊢ (𝐴 ⊆ (V × V) →
(𝑥 ∈ 𝐴 → 𝑥 ∈ (V × V))) |
12 | 10, 11 | sylbi 216 |
. . . . . . . 8
⊢ (Rel
𝐴 → (𝑥 ∈ 𝐴 → 𝑥 ∈ (V × V))) |
13 | 12 | imp 408 |
. . . . . . 7
⊢ ((Rel
𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ (V × V)) |
14 | | op1steq 7966 |
. . . . . . 7
⊢ (𝑥 ∈ (V × V) →
((1st ‘𝑥)
= 𝐵 ↔ ∃𝑦 𝑥 = ⟨𝐵, 𝑦⟩)) |
15 | 13, 14 | syl 17 |
. . . . . 6
⊢ ((Rel
𝐴 ∧ 𝑥 ∈ 𝐴) → ((1st ‘𝑥) = 𝐵 ↔ ∃𝑦 𝑥 = ⟨𝐵, 𝑦⟩)) |
16 | 15 | rexbidva 3174 |
. . . . 5
⊢ (Rel
𝐴 → (∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐵 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 𝑥 = ⟨𝐵, 𝑦⟩)) |
17 | 16 | adantr 482 |
. . . 4
⊢ ((Rel
𝐴 ∧ 𝐵 ∈ V) → (∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐵 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 𝑥 = ⟨𝐵, 𝑦⟩)) |
18 | | rexcom4 3272 |
. . . . 5
⊢
(∃𝑥 ∈
𝐴 ∃𝑦 𝑥 = ⟨𝐵, 𝑦⟩ ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝑥 = ⟨𝐵, 𝑦⟩) |
19 | | risset 3222 |
. . . . . 6
⊢
(⟨𝐵, 𝑦⟩ ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑥 = ⟨𝐵, 𝑦⟩) |
20 | 19 | exbii 1851 |
. . . . 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 801 |
1
⊢ (Rel
𝐴 → (𝐵 ∈ dom 𝐴 ↔ ∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐵)) |