Metamath Proof Explorer

Theorem relssdmrnOLD

Description: Obsolete version of relssdmrn as of 23-Dec-2024. (Contributed by NM, 3-Aug-1994) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion relssdmrnOLD 
|- ( Rel A -> A C_ ( dom A X. ran A ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( Rel A -> Rel A )
2 19.8a 
 |-  ( <. x , y >. e. A -> E. y <. x , y >. e. A )
3 19.8a 
 |-  ( <. x , y >. e. A -> E. x <. x , y >. e. A )
4 opelxp 
 |-  ( <. x , y >. e. ( dom A X. ran A ) <-> ( x e. dom A /\ y e. ran A ) )
5 vex 
 |-  x e. _V
6 5 eldm2 
 |-  ( x e. dom A <-> E. y <. x , y >. e. A )
7 vex 
 |-  y e. _V
8 7 elrn2 
 |-  ( y e. ran A <-> E. x <. x , y >. e. A )
9 6 8 anbi12i 
 |-  ( ( x e. dom A /\ y e. ran A ) <-> ( E. y <. x , y >. e. A /\ E. x <. x , y >. e. A ) )
10 4 9 bitri 
 |-  ( <. x , y >. e. ( dom A X. ran A ) <-> ( E. y <. x , y >. e. A /\ E. x <. x , y >. e. A ) )
11 2 3 10 sylanbrc 
 |-  ( <. x , y >. e. A -> <. x , y >. e. ( dom A X. ran A ) )
12 11 a1i 
 |-  ( Rel A -> ( <. x , y >. e. A -> <. x , y >. e. ( dom A X. ran A ) ) )
13 1 12 relssdv 
 |-  ( Rel A -> A C_ ( dom A X. ran A ) )