MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  enrefg Structured version   Unicode version

Theorem enrefg 7329
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  |-  ( A  e.  V  ->  A  ~~  A )

Proof of Theorem enrefg
StepHypRef Expression
1 f1oi 5664 . . 3  |-  (  _I  |`  A ) : A -1-1-onto-> A
2 f1oen2g 7314 . . 3  |-  ( ( A  e.  V  /\  A  e.  V  /\  (  _I  |`  A ) : A -1-1-onto-> A )  ->  A  ~~  A )
31, 2mp3an3 1296 . 2  |-  ( ( A  e.  V  /\  A  e.  V )  ->  A  ~~  A )
43anidms 638 1  |-  ( A  e.  V  ->  A  ~~  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1755   class class class wbr 4280    _I cid 4618    |` cres 4829   -1-1-onto->wf1o 5405    ~~ cen 7295
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-id 4623  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-en 7299
This theorem is referenced by:  enref  7330  eqeng  7331  domrefg  7332  difsnen  7381  sdomirr  7436  mapdom1  7464  mapdom2  7470  onfin  7489  ssnnfi  7520  infdifsn  7850  infdiffi  7851  onenon  8107  cardonle  8115  cda1en  8332  xpcdaen  8340  mapcdaen  8341  onacda  8354  ssfin4  8467  canthp1lem1  8806  gchhar  8833  hashfac  12194  mreexexlem3d  14566  cyggenod  16340  fidomndrnglem  17299  mdetunilem8  18266  frlmpwfi  29295  fiuneneq  29404
  Copyright terms: Public domain W3C validator