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 ∈ A 1 st ⁡ 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 ⊢ 1 st ⁡ x = B → 1 st ⁡ x = B
4 fvex ⊢ 1 st ⁡ x ∈ V
5 3 4 eqeltrrdi ⊢ 1 st ⁡ x = B → B ∈ V
6 5 rexlimivw ⊢ ∃ x ∈ A 1 st ⁡ x = B → B ∈ V
7 6 anim2i ⊢ Rel ⁡ A ∧ ∃ x ∈ A 1 st ⁡ x = B → Rel ⁡ A ∧ B ∈ V
8 eldm2g ⊢ B ∈ V → B ∈ dom ⁡ A ↔ ∃ y B y ∈ A
9 8 adantl ⊢ Rel ⁡ A ∧ B ∈ V → B ∈ dom ⁡ A ↔ ∃ y B y ∈ 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 → 1 st ⁡ x = B ↔ ∃ y x = B y
15 13 14 syl ⊢ Rel ⁡ A ∧ x ∈ A → 1 st ⁡ x = B ↔ ∃ y x = B y
16 15 rexbidva ⊢ Rel ⁡ A → ∃ x ∈ A 1 st ⁡ x = B ↔ ∃ x ∈ A ∃ y x = B y
17 16 adantr ⊢ Rel ⁡ A ∧ B ∈ V → ∃ x ∈ A 1 st ⁡ x = B ↔ ∃ x ∈ A ∃ y x = B y
18 rexcom4 ⊢ ∃ x ∈ A ∃ y x = B y ↔ ∃ y ∃ x ∈ A x = B y
19 risset ⊢ B y ∈ A ↔ ∃ x ∈ A x = B y
20 19 exbii ⊢ ∃ y B y ∈ A ↔ ∃ y ∃ x ∈ A x = B y
21 18 20 bitr4i ⊢ ∃ x ∈ A ∃ y x = B y ↔ ∃ y B y ∈ A
22 17 21 bitrdi ⊢ Rel ⁡ A ∧ B ∈ V → ∃ x ∈ A 1 st ⁡ x = B ↔ ∃ y B y ∈ A
23 9 22 bitr4d ⊢ Rel ⁡ A ∧ B ∈ V → B ∈ dom ⁡ A ↔ ∃ x ∈ A 1 st ⁡ x = B
24 2 7 23 pm5.21nd ⊢ Rel ⁡ A → B ∈ dom ⁡ A ↔ ∃ x ∈ A 1 st ⁡ x = B