Metamath Proof Explorer

Theorem f1imaeng

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 Mario Carneiro, 15-May-2015)

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

Proof

Step	Hyp	Ref	Expression
1		f1ores	$⊢ (F : A \underset{1-1}{⟶} B \land C \subseteq A) \to ({F ↾}_{C}) : C \underset{1-1 onto}{⟶} F [C]$
2		f1oeng	$⊢ (C \in V \land ({F ↾}_{C}) : C \underset{1-1 onto}{⟶} F [C]) \to C \approx F [C]$
3	2	ancoms	$⊢ (({F ↾}_{C}) : C \underset{1-1 onto}{⟶} F [C] \land C \in V) \to C \approx F [C]$
4	1 3	stoic3	$⊢ (F : A \underset{1-1}{⟶} B \land C \subseteq A \land C \in V) \to C \approx F [C]$
5	4	ensymd	$⊢ (F : A \underset{1-1}{⟶} B \land C \subseteq A \land C \in V) \to F [C] \approx C$