Step | Hyp | Ref
| Expression |
1 | | elex 2748 |
. . 3
⊢ (𝐵 ∈ dom 𝐴 → 𝐵 ∈ V) |
2 | 1 | anim2i 342 |
. 2
⊢ ((Rel
𝐴 ∧ 𝐵 ∈ dom 𝐴) → (Rel 𝐴 ∧ 𝐵 ∈ V)) |
3 | | id 19 |
. . . . 5
⊢
((1st ‘𝑥) = 𝐵 → (1st ‘𝑥) = 𝐵) |
4 | | vex 2740 |
. . . . . 6
⊢ 𝑥 ∈ V |
5 | | 1stexg 6167 |
. . . . . 6
⊢ (𝑥 ∈ V → (1st
‘𝑥) ∈
V) |
6 | 4, 5 | ax-mp 5 |
. . . . 5
⊢
(1st ‘𝑥) ∈ V |
7 | 3, 6 | eqeltrrdi 2269 |
. . . 4
⊢
((1st ‘𝑥) = 𝐵 → 𝐵 ∈ V) |
8 | 7 | rexlimivw 2590 |
. . 3
⊢
(∃𝑥 ∈
𝐴 (1st
‘𝑥) = 𝐵 → 𝐵 ∈ V) |
9 | 8 | anim2i 342 |
. 2
⊢ ((Rel
𝐴 ∧ ∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐵) → (Rel 𝐴 ∧ 𝐵 ∈ V)) |
10 | | eldm2g 4823 |
. . . 4
⊢ (𝐵 ∈ V → (𝐵 ∈ dom 𝐴 ↔ ∃𝑦⟨𝐵, 𝑦⟩ ∈ 𝐴)) |
11 | 10 | adantl 277 |
. . 3
⊢ ((Rel
𝐴 ∧ 𝐵 ∈ V) → (𝐵 ∈ dom 𝐴 ↔ ∃𝑦⟨𝐵, 𝑦⟩ ∈ 𝐴)) |
12 | | df-rel 4633 |
. . . . . . . . 9
⊢ (Rel
𝐴 ↔ 𝐴 ⊆ (V × V)) |
13 | | ssel 3149 |
. . . . . . . . 9
⊢ (𝐴 ⊆ (V × V) →
(𝑥 ∈ 𝐴 → 𝑥 ∈ (V × V))) |
14 | 12, 13 | sylbi 121 |
. . . . . . . 8
⊢ (Rel
𝐴 → (𝑥 ∈ 𝐴 → 𝑥 ∈ (V × V))) |
15 | 14 | imp 124 |
. . . . . . 7
⊢ ((Rel
𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ (V × V)) |
16 | | op1steq 6179 |
. . . . . . 7
⊢ (𝑥 ∈ (V × V) →
((1st ‘𝑥)
= 𝐵 ↔ ∃𝑦 𝑥 = ⟨𝐵, 𝑦⟩)) |
17 | 15, 16 | syl 14 |
. . . . . 6
⊢ ((Rel
𝐴 ∧ 𝑥 ∈ 𝐴) → ((1st ‘𝑥) = 𝐵 ↔ ∃𝑦 𝑥 = ⟨𝐵, 𝑦⟩)) |
18 | 17 | rexbidva 2474 |
. . . . 5
⊢ (Rel
𝐴 → (∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐵 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 𝑥 = ⟨𝐵, 𝑦⟩)) |
19 | 18 | adantr 276 |
. . . 4
⊢ ((Rel
𝐴 ∧ 𝐵 ∈ V) → (∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐵 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 𝑥 = ⟨𝐵, 𝑦⟩)) |
20 | | rexcom4 2760 |
. . . . 5
⊢
(∃𝑥 ∈
𝐴 ∃𝑦 𝑥 = ⟨𝐵, 𝑦⟩ ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝑥 = ⟨𝐵, 𝑦⟩) |
21 | | risset 2505 |
. . . . . 6
⊢
(⟨𝐵, 𝑦⟩ ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑥 = ⟨𝐵, 𝑦⟩) |
22 | 21 | exbii 1605 |
. . . . 5
⊢
(∃𝑦⟨𝐵, 𝑦⟩ ∈ 𝐴 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝑥 = ⟨𝐵, 𝑦⟩) |
23 | 20, 22 | bitr4i 187 |
. . . 4
⊢
(∃𝑥 ∈
𝐴 ∃𝑦 𝑥 = ⟨𝐵, 𝑦⟩ ↔ ∃𝑦⟨𝐵, 𝑦⟩ ∈ 𝐴) |
24 | 19, 23 | bitrdi 196 |
. . 3
⊢ ((Rel
𝐴 ∧ 𝐵 ∈ V) → (∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐵 ↔ ∃𝑦⟨𝐵, 𝑦⟩ ∈ 𝐴)) |
25 | 11, 24 | bitr4d 191 |
. 2
⊢ ((Rel
𝐴 ∧ 𝐵 ∈ V) → (𝐵 ∈ dom 𝐴 ↔ ∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐵)) |
26 | 2, 9, 25 | pm5.21nd 916 |
1
⊢ (Rel
𝐴 → (𝐵 ∈ dom 𝐴 ↔ ∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐵)) |