Metamath Proof Explorer


Theorem reldm

Description: An expression for the domain of a relation. (Contributed by NM, 22-Sep-2013)

Ref Expression
Assertion reldm Rel A dom A = ran x A 1 st x

Proof

Step Hyp Ref Expression
1 releldm2 Rel A y dom A z A 1 st z = y
2 fvex 1 st x V
3 eqid x A 1 st x = x A 1 st x
4 2 3 fnmpti x A 1 st x Fn A
5 fvelrnb x A 1 st x Fn A y ran x A 1 st x z A x A 1 st x z = y
6 4 5 ax-mp y ran x A 1 st x z A x A 1 st x z = y
7 fveq2 x = z 1 st x = 1 st z
8 fvex 1 st z V
9 7 3 8 fvmpt z A x A 1 st x z = 1 st z
10 9 eqeq1d z A x A 1 st x z = y 1 st z = y
11 10 rexbiia z A x A 1 st x z = y z A 1 st z = y
12 11 a1i Rel A z A x A 1 st x z = y z A 1 st z = y
13 6 12 bitr2id Rel A z A 1 st z = y y ran x A 1 st x
14 1 13 bitrd Rel A y dom A y ran x A 1 st x
15 14 eqrdv Rel A dom A = ran x A 1 st x