Theorem enrefg 8954

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

Assertion

Ref	Expression
enrefg	⊢ (𝐴 ∈ 𝑉 → 𝐴 ≈ 𝐴)

Proof of Theorem enrefg

Step	Hyp	Ref	Expression
1		f1oi 6834	. . 3 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴
2		f1oen2g 8938	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴) → 𝐴 ≈ 𝐴)
3	1, 2	mp3an3 1465	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → 𝐴 ≈ 𝐴)
4	3	anidms 573	1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ≈ 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2136   class class class wbr 5094   I cid 5534   ↾ cres 5642  –1-1-onto→wf1o 6509   ≈ cen 8913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728  ax-sep 5240  ax-pow 5316  ax-pr 5384  ax-un 7707

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-ral 3071  df-rex 3081  df-rab 3409  df-v 3450  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4281  df-if 4475  df-pw 4551  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5095  df-opab 5157  df-id 5535  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-rn 5651  df-res 5652  df-ima 5653  df-fun 6512  df-fn 6513  df-f 6514  df-f1 6515  df-fo 6516  df-f1o 6517  df-en 8917

This theorem is referenced by:  enref  8955  eqeng  8956  domrefg  8957  difsnen  9020  sdomirr  9075  mapdom1  9103  mapdom2  9109  rneqdmfinf1o  9266  infdifsn  9602  infdiffi  9603  onenon  9897  cardonle  9905  dju1en  10118  xpdjuen  10126  mapdjuen  10127  onadju  10140  nnadju  10144  ssfin4  10257  canthp1lem1  10600  gchhar  10627  hashfac  14461  mreexexlem3d  17654  cyggenod  19900  mdetunilem8  22652  frlmpwfi  43623  fiuneneq  43717  enrelmap  44521