Theorem enrefg

Description: Equinumerosity is reflexive. Theorem 1 of Suppes p. 92. (Contributed by NM, 18-Jun-1998) (Revised by Mario Carneiro, 26-Apr-2015)

	Ref	Expression
Assertion	enrefg	$$⊢A\in V\to A\approx A$$

Proof

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