Theorem hashimaf1

Description: Taking the image of a set by a one-to-one function does not affect size. (Contributed by Thierry Arnoux, 18-Jan-2026)

	Ref	Expression
Hypotheses	hashimaf1.1	$$⊢\phi \to F:A\underset{1-1}{⟶}B$$
	hashimaf1.2	$$⊢\phi \to C\subseteq A$$
	hashimaf1.3	$$⊢\phi \to A\in V$$
Assertion	hashimaf1	$$⊢\phi \to \left|F\left[C\right]\right|=\left|C\right|$$

Proof

Step	Hyp	Ref	Expression
1		hashimaf1.1	$$⊢\phi \to F:A\underset{1-1}{⟶}B$$
2		hashimaf1.2	$$⊢\phi \to C\subseteq A$$
3		hashimaf1.3	$$⊢\phi \to A\in V$$
4	3 2	sselpwd	$$⊢\phi \to C\in 𝒫A$$
5		f1ores	$$⊢\left(F:A\underset{1-1}{⟶}B\wedge C\subseteq A\right)\to \left({F\upharpoonright }_C\right):C\underset{1-1\; onto}{⟶}F\left[C\right]$$
6	1 2 5	syl2anc	$$⊢\phi \to \left({F\upharpoonright }_C\right):C\underset{1-1\; onto}{⟶}F\left[C\right]$$
7		f1oeng	$$⊢\left(C\in 𝒫A\wedge \left({F\upharpoonright }_C\right):C\underset{1-1\; onto}{⟶}F\left[C\right]\right)\to C\approx F\left[C\right]$$
8	4 6 7	syl2anc	$$⊢\phi \to C\approx F\left[C\right]$$
9	8	ensymd	$$⊢\phi \to F\left[C\right]\approx C$$
10		hasheni	$$⊢F\left[C\right]\approx C\to \left|F\left[C\right]\right|=\left|C\right|$$
11	9 10	syl	$$⊢\phi \to \left|F\left[C\right]\right|=\left|C\right|$$