Metamath Proof Explorer

Theorem cnvssrndm

Description: The converse is a subset of the cartesian product of range and domain. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Assertion cnvssrndm 
|- `' A C_ ( ran A X. dom A )

Proof

Step Hyp Ref Expression
1 relcnv 
 |-  Rel `' A
2 relssdmrn 
 |-  ( Rel `' A -> `' A C_ ( dom `' A X. ran `' A ) )
3 1 2 ax-mp 
 |-  `' A C_ ( dom `' A X. ran `' A )
4 df-rn 
 |-  ran A = dom `' A
5 dfdm4 
 |-  dom A = ran `' A
6 4 5 xpeq12i 
 |-  ( ran A X. dom A ) = ( dom `' A X. ran `' A )
7 3 6 sseqtrri 
 |-  `' A C_ ( ran A X. dom A )