Theorem enrefg 8564

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 6643	. . 3 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴
2		f1oen2g 8549	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴) → 𝐴 ≈ 𝐴)
3	1, 2	mp3an3 1447	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → 𝐴 ≈ 𝐴)
4	3	anidms 570	1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ≈ 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2111   class class class wbr 5035   I cid 5432   ↾ cres 5529  –1-1-onto→wf1o 6338   ≈ cen 8529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5172  ax-nul 5179  ax-pow 5237  ax-pr 5301  ax-un 7464

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ral 3075  df-rex 3076  df-rab 3079  df-v 3411  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5036  df-opab 5098  df-id 5433  df-xp 5533  df-rel 5534  df-cnv 5535  df-co 5536  df-dm 5537  df-rn 5538  df-res 5539  df-ima 5540  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-en 8533

This theorem is referenced by:  enref  8565  eqeng  8566  domrefg  8567  difsnen  8625  sdomirr  8681  mapdom1  8709  mapdom2  8715  onfin  8753  rneqdmfinf1o  8838  infdifsn  9158  infdiffi  9159  onenon  9416  cardonle  9424  dju1en  9636  xpdjuen  9644  mapdjuen  9645  onadju  9658  nnadju  9662  ssfin4  9775  canthp1lem1  10117  gchhar  10144  hashfac  13873  mreexexlem3d  16980  cyggenod  19076  fidomndrnglem  20152  mdetunilem8  21324  frlmpwfi  40443  fiuneneq  40542  enrelmap  41099