Step | Hyp | Ref
| Expression |
1 | | elex 2723 |
. . 3
⊢ (𝐵 ∈ dom 𝐴 → 𝐵 ∈ V) |
2 | 1 | anim2i 340 |
. 2
⊢ ((Rel
𝐴 ∧ 𝐵 ∈ dom 𝐴) → (Rel 𝐴 ∧ 𝐵 ∈ V)) |
3 | | id 19 |
. . . . 5
⊢
((1st ‘𝑥) = 𝐵 → (1st ‘𝑥) = 𝐵) |
4 | | vex 2715 |
. . . . . 6
⊢ 𝑥 ∈ V |
5 | | 1stexg 6115 |
. . . . . 6
⊢ (𝑥 ∈ V → (1st
‘𝑥) ∈
V) |
6 | 4, 5 | ax-mp 5 |
. . . . 5
⊢
(1st ‘𝑥) ∈ V |
7 | 3, 6 | eqeltrrdi 2249 |
. . . 4
⊢
((1st ‘𝑥) = 𝐵 → 𝐵 ∈ V) |
8 | 7 | rexlimivw 2570 |
. . 3
⊢
(∃𝑥 ∈
𝐴 (1st
‘𝑥) = 𝐵 → 𝐵 ∈ V) |
9 | 8 | anim2i 340 |
. 2
⊢ ((Rel
𝐴 ∧ ∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐵) → (Rel 𝐴 ∧ 𝐵 ∈ V)) |
10 | | eldm2g 4782 |
. . . 4
⊢ (𝐵 ∈ V → (𝐵 ∈ dom 𝐴 ↔ ∃𝑦〈𝐵, 𝑦〉 ∈ 𝐴)) |
11 | 10 | adantl 275 |
. . 3
⊢ ((Rel
𝐴 ∧ 𝐵 ∈ V) → (𝐵 ∈ dom 𝐴 ↔ ∃𝑦〈𝐵, 𝑦〉 ∈ 𝐴)) |
12 | | df-rel 4593 |
. . . . . . . . 9
⊢ (Rel
𝐴 ↔ 𝐴 ⊆ (V × V)) |
13 | | ssel 3122 |
. . . . . . . . 9
⊢ (𝐴 ⊆ (V × V) →
(𝑥 ∈ 𝐴 → 𝑥 ∈ (V × V))) |
14 | 12, 13 | sylbi 120 |
. . . . . . . 8
⊢ (Rel
𝐴 → (𝑥 ∈ 𝐴 → 𝑥 ∈ (V × V))) |
15 | 14 | imp 123 |
. . . . . . 7
⊢ ((Rel
𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ (V × V)) |
16 | | op1steq 6127 |
. . . . . . 7
⊢ (𝑥 ∈ (V × V) →
((1st ‘𝑥)
= 𝐵 ↔ ∃𝑦 𝑥 = 〈𝐵, 𝑦〉)) |
17 | 15, 16 | syl 14 |
. . . . . 6
⊢ ((Rel
𝐴 ∧ 𝑥 ∈ 𝐴) → ((1st ‘𝑥) = 𝐵 ↔ ∃𝑦 𝑥 = 〈𝐵, 𝑦〉)) |
18 | 17 | rexbidva 2454 |
. . . . 5
⊢ (Rel
𝐴 → (∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐵 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 𝑥 = 〈𝐵, 𝑦〉)) |
19 | 18 | adantr 274 |
. . . 4
⊢ ((Rel
𝐴 ∧ 𝐵 ∈ V) → (∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐵 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 𝑥 = 〈𝐵, 𝑦〉)) |
20 | | rexcom4 2735 |
. . . . 5
⊢
(∃𝑥 ∈
𝐴 ∃𝑦 𝑥 = 〈𝐵, 𝑦〉 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝑥 = 〈𝐵, 𝑦〉) |
21 | | risset 2485 |
. . . . . 6
⊢
(〈𝐵, 𝑦〉 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑥 = 〈𝐵, 𝑦〉) |
22 | 21 | exbii 1585 |
. . . . 5
⊢
(∃𝑦〈𝐵, 𝑦〉 ∈ 𝐴 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝑥 = 〈𝐵, 𝑦〉) |
23 | 20, 22 | bitr4i 186 |
. . . 4
⊢
(∃𝑥 ∈
𝐴 ∃𝑦 𝑥 = 〈𝐵, 𝑦〉 ↔ ∃𝑦〈𝐵, 𝑦〉 ∈ 𝐴) |
24 | 19, 23 | bitrdi 195 |
. . 3
⊢ ((Rel
𝐴 ∧ 𝐵 ∈ V) → (∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐵 ↔ ∃𝑦〈𝐵, 𝑦〉 ∈ 𝐴)) |
25 | 11, 24 | bitr4d 190 |
. 2
⊢ ((Rel
𝐴 ∧ 𝐵 ∈ V) → (𝐵 ∈ dom 𝐴 ↔ ∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐵)) |
26 | 2, 9, 25 | pm5.21nd 902 |
1
⊢ (Rel
𝐴 → (𝐵 ∈ dom 𝐴 ↔ ∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐵)) |