Step | Hyp | Ref
| Expression |
1 | | elex 2566 |
. . 3
⊢ (𝐵 ∈ dom 𝐴 → 𝐵 ∈ V) |
2 | 1 | anim2i 324 |
. 2
⊢ ((Rel
𝐴 ∧ 𝐵 ∈ dom 𝐴) → (Rel 𝐴 ∧ 𝐵 ∈ V)) |
3 | | id 19 |
. . . . 5
⊢
((1st ‘𝑥) = 𝐵 → (1st ‘𝑥) = 𝐵) |
4 | | vex 2560 |
. . . . . 6
⊢ 𝑥 ∈ V |
5 | | 1stexg 5794 |
. . . . . 6
⊢ (𝑥 ∈ V → (1st
‘𝑥) ∈
V) |
6 | 4, 5 | ax-mp 7 |
. . . . 5
⊢
(1st ‘𝑥) ∈ V |
7 | 3, 6 | syl6eqelr 2129 |
. . . 4
⊢
((1st ‘𝑥) = 𝐵 → 𝐵 ∈ V) |
8 | 7 | rexlimivw 2429 |
. . 3
⊢
(∃𝑥 ∈
𝐴 (1st
‘𝑥) = 𝐵 → 𝐵 ∈ V) |
9 | 8 | anim2i 324 |
. 2
⊢ ((Rel
𝐴 ∧ ∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐵) → (Rel 𝐴 ∧ 𝐵 ∈ V)) |
10 | | eldm2g 4531 |
. . . 4
⊢ (𝐵 ∈ V → (𝐵 ∈ dom 𝐴 ↔ ∃𝑦〈𝐵, 𝑦〉 ∈ 𝐴)) |
11 | 10 | adantl 262 |
. . 3
⊢ ((Rel
𝐴 ∧ 𝐵 ∈ V) → (𝐵 ∈ dom 𝐴 ↔ ∃𝑦〈𝐵, 𝑦〉 ∈ 𝐴)) |
12 | | df-rel 4352 |
. . . . . . . . 9
⊢ (Rel
𝐴 ↔ 𝐴 ⊆ (V × V)) |
13 | | ssel 2939 |
. . . . . . . . 9
⊢ (𝐴 ⊆ (V × V) →
(𝑥 ∈ 𝐴 → 𝑥 ∈ (V × V))) |
14 | 12, 13 | sylbi 114 |
. . . . . . . 8
⊢ (Rel
𝐴 → (𝑥 ∈ 𝐴 → 𝑥 ∈ (V × V))) |
15 | 14 | imp 115 |
. . . . . . 7
⊢ ((Rel
𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ (V × V)) |
16 | | op1steq 5805 |
. . . . . . 7
⊢ (𝑥 ∈ (V × V) →
((1st ‘𝑥)
= 𝐵 ↔ ∃𝑦 𝑥 = 〈𝐵, 𝑦〉)) |
17 | 15, 16 | syl 14 |
. . . . . 6
⊢ ((Rel
𝐴 ∧ 𝑥 ∈ 𝐴) → ((1st ‘𝑥) = 𝐵 ↔ ∃𝑦 𝑥 = 〈𝐵, 𝑦〉)) |
18 | 17 | rexbidva 2323 |
. . . . 5
⊢ (Rel
𝐴 → (∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐵 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 𝑥 = 〈𝐵, 𝑦〉)) |
19 | 18 | adantr 261 |
. . . 4
⊢ ((Rel
𝐴 ∧ 𝐵 ∈ V) → (∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐵 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 𝑥 = 〈𝐵, 𝑦〉)) |
20 | | rexcom4 2577 |
. . . . 5
⊢
(∃𝑥 ∈
𝐴 ∃𝑦 𝑥 = 〈𝐵, 𝑦〉 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝑥 = 〈𝐵, 𝑦〉) |
21 | | risset 2352 |
. . . . . 6
⊢
(〈𝐵, 𝑦〉 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑥 = 〈𝐵, 𝑦〉) |
22 | 21 | exbii 1496 |
. . . . 5
⊢
(∃𝑦〈𝐵, 𝑦〉 ∈ 𝐴 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝑥 = 〈𝐵, 𝑦〉) |
23 | 20, 22 | bitr4i 176 |
. . . 4
⊢
(∃𝑥 ∈
𝐴 ∃𝑦 𝑥 = 〈𝐵, 𝑦〉 ↔ ∃𝑦〈𝐵, 𝑦〉 ∈ 𝐴) |
24 | 19, 23 | syl6bb 185 |
. . 3
⊢ ((Rel
𝐴 ∧ 𝐵 ∈ V) → (∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐵 ↔ ∃𝑦〈𝐵, 𝑦〉 ∈ 𝐴)) |
25 | 11, 24 | bitr4d 180 |
. 2
⊢ ((Rel
𝐴 ∧ 𝐵 ∈ V) → (𝐵 ∈ dom 𝐴 ↔ ∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐵)) |
26 | 2, 9, 25 | pm5.21nd 825 |
1
⊢ (Rel
𝐴 → (𝐵 ∈ dom 𝐴 ↔ ∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐵)) |