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	⊢ ( ◡ 𝐴 “ 𝐵 ) ⊆ dom 𝐴

Proof

Step	Hyp	Ref	Expression
1		imassrn	⊢ ( ◡ 𝐴 “ 𝐵 ) ⊆ ran ◡ 𝐴
2		dfdm4	⊢ dom 𝐴 = ran ◡ 𝐴
3	1 2	sseqtrri	⊢ ( ◡ 𝐴 “ 𝐵 ) ⊆ dom 𝐴