Metamath Proof Explorer

Theorem f1imaen

Description: If a function is one-to-one, then the image of a subset of its domain under it is equinumerous to the subset. (Contributed by NM, 30-Sep-2004)

		Ref	Expression
	Hypothesis	f1imaen.1	$⊢ C \in V$
	Assertion	f1imaen	$⊢ (F : A \underset{1-1}{⟶} B \land C \subseteq A) \to F [C] \approx C$

Proof

Step	Hyp	Ref	Expression
1		f1imaen.1	$⊢ C \in V$
2		f1imaeng	$⊢ (F : A \underset{1-1}{⟶} B \land C \subseteq A \land C \in V) \to F [C] \approx C$
3	1 2	mp3an3	$⊢ (F : A \underset{1-1}{⟶} B \land C \subseteq A) \to F [C] \approx C$