Metamath Proof Explorer

Theorem releldm2

Description: Two ways of expressing membership in the domain of a relation. (Contributed by NM, 22-Sep-2013)

Ref Expression
Assertion releldm2 ⊢Rel⁡A→B∈dom⁡A↔∃x∈A1st⁡x=B

Proof

Step Hyp Ref Expression
1 elex ⊢B∈dom⁡A→B∈V
2 1 anim2i ⊢Rel⁡A∧B∈dom⁡A→Rel⁡A∧B∈V
3 id ⊢1st⁡x=B→1st⁡x=B
4 fvex ⊢1st⁡x∈V
5 3 4 eqeltrrdi ⊢1st⁡x=B→B∈V
6 5 rexlimivw ⊢∃x∈A1st⁡x=B→B∈V
7 6 anim2i ⊢Rel⁡A∧∃x∈A1st⁡x=B→Rel⁡A∧B∈V
8 eldm2g ⊢B∈V→B∈dom⁡A↔∃yBy∈A
9 8 adantl ⊢Rel⁡A∧B∈V→B∈dom⁡A↔∃yBy∈A
10 df-rel ⊢Rel⁡A↔A⊆V×V
11 ssel ⊢A⊆V×V→x∈A→x∈V×V
12 10 11 sylbi ⊢Rel⁡A→x∈A→x∈V×V
13 12 imp ⊢Rel⁡A∧x∈A→x∈V×V
14 op1steq ⊢x∈V×V→1st⁡x=B↔∃yx=By
15 13 14 syl ⊢Rel⁡A∧x∈A→1st⁡x=B↔∃yx=By
16 15 rexbidva ⊢Rel⁡A→∃x∈A1st⁡x=B↔∃x∈A∃yx=By
17 16 adantr ⊢Rel⁡A∧B∈V→∃x∈A1st⁡x=B↔∃x∈A∃yx=By
18 rexcom4 ⊢∃x∈A∃yx=By↔∃y∃x∈Ax=By
19 risset ⊢By∈A↔∃x∈Ax=By
20 19 exbii ⊢∃yBy∈A↔∃y∃x∈Ax=By
21 18 20 bitr4i ⊢∃x∈A∃yx=By↔∃yBy∈A
22 17 21 bitrdi ⊢Rel⁡A∧B∈V→∃x∈A1st⁡x=B↔∃yBy∈A
23 9 22 bitr4d ⊢Rel⁡A∧B∈V→B∈dom⁡A↔∃x∈A1st⁡x=B
24 2 7 23 pm5.21nd ⊢Rel⁡A→B∈dom⁡A↔∃x∈A1st⁡x=B