Metamath Proof Explorer

Theorem cnvimass

Description: A preimage under any class is included in the domain of the class. (Contributed by FL, 29-Jan-2007)

Ref Expression
Assertion cnvimass 
|- ( `' A " B ) C_ dom A

Proof

Step Hyp Ref Expression
1 imassrn 
 |-  ( `' A " B ) C_ ran `' A
2 dfdm4 
 |-  dom A = ran `' A
3 1 2 sseqtrri 
 |-  ( `' A " B ) C_ dom A