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