Metamath Proof Explorer

Theorem reldm

Description: An expression for the domain of a relation. (Contributed by NM, 22-Sep-2013) (Proof shortened by Sky Winter, 22-Oct-2026)

Ref Expression
Assertion reldm 
|- ( Rel A -> dom A = ran ( x e. A |-> ( 1st ` x ) ) )

Proof

Step Hyp Ref Expression
1 releldm2 
 |-  ( Rel A -> ( y e. dom A <-> E. x e. A ( 1st ` x ) = y ) )
2 eqid 
 |-  ( x e. A |-> ( 1st ` x ) ) = ( x e. A |-> ( 1st ` x ) )
3 fvex 
 |-  ( 1st ` x ) e. _V
4 2 3 elrnmpti 
 |-  ( y e. ran ( x e. A |-> ( 1st ` x ) ) <-> E. x e. A y = ( 1st ` x ) )
5 eqcom 
 |-  ( y = ( 1st ` x ) <-> ( 1st ` x ) = y )
6 5 rexbii 
 |-  ( E. x e. A y = ( 1st ` x ) <-> E. x e. A ( 1st ` x ) = y )
7 4 6 bitri 
 |-  ( y e. ran ( x e. A |-> ( 1st ` x ) ) <-> E. x e. A ( 1st ` x ) = y )
8 1 7 bitr4di 
 |-  ( Rel A -> ( y e. dom A <-> y e. ran ( x e. A |-> ( 1st ` x ) ) ) )
9 8 eqrdv 
 |-  ( Rel A -> dom A = ran ( x e. A |-> ( 1st ` x ) ) )