This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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^{-1} [B] \subseteq dom A$

Step	Hyp	Ref	Expression
1		imassrn	$⊢ A^{-1} [B] \subseteq ran A^{-1}$
2		dfdm4	$⊢ dom A = ran A^{-1}$
3	1 2	sseqtrri	$⊢ A^{-1} [B] \subseteq dom A$