Theorem enreffi

Description: Equinumerosity is reflexive for finite sets, proved without using the Axiom of Power Sets (unlike enrefg ). (Contributed by BTernaryTau, 8-Sep-2024)

	Ref	Expression
Assertion	enreffi	$$⊢A\in \mathrm{Fin}\to A\approx A$$

Proof

Step	Hyp	Ref	Expression
1		f1oi	$$⊢\left({\mathrm{I}\upharpoonright }_A\right):A\underset{1-1\; onto}{⟶}A$$
2		f1oenfi	$$⊢\left(A\in \mathrm{Fin}\wedge \left({\mathrm{I}\upharpoonright }_A\right):A\underset{1-1\; onto}{⟶}A\right)\to A\approx A$$
3	1 2	mpan2	$$⊢A\in \mathrm{Fin}\to A\approx A$$