Theorem enref

Description: Equinumerosity is reflexive. Theorem 1 of Suppes p. 92. (Contributed by NM, 25-Sep-2004)

	Ref	Expression
Hypothesis	enref.1	⊢ 𝐴 ∈ V
Assertion	enref	⊢ 𝐴 ≈ 𝐴

Proof

Step	Hyp	Ref	Expression
1		enref.1	⊢ 𝐴 ∈ V
2		enrefg	⊢ ( 𝐴 ∈ V → 𝐴 ≈ 𝐴 )
3	1 2	ax-mp	⊢ 𝐴 ≈ 𝐴