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

Theorem ensym 6905
Description: Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
Assertion
Ref Expression
ensym  |-  ( A 
~~  B  ->  B  ~~  A )

Proof of Theorem ensym
StepHypRef Expression
1 ensymb 6904 . 2  |-  ( A 
~~  B  <->  B  ~~  A )
21biimpi 188 1  |-  ( A 
~~  B  ->  B  ~~  A )
Colors of variables: wff set class
Syntax hints:    -> wi 6   class class class wbr 4024    ~~ cen 6855
This theorem is referenced by:  ensymi  6906  ensymd  6907  f1imaeng  6916  f1imaen2g  6917  en2sn  6935  xpdom3  6955  omxpen  6959  sbthb  6977  domnsym  6982  sdomdomtr  6989  domsdomtr  6991  enen1  6996  enen2  6997  domen1  6998  domen2  6999  sdomen1  7000  sdomen2  7001  domtriord  7002  xpen  7019  mapdom2  7027  mapdom3  7028  pwen  7029  limensuci  7032  phplem4  7038  nneneq  7039  php  7040  php2  7041  php3  7042  unxpdom2  7066  sucxpdom  7067  ominf  7070  fineqvlem  7072  en1eqsn  7083  dif1enOLD  7085  dif1en  7086  enp1i  7088  findcard3  7095  isfinite2  7110  nnsdomg  7111  domunfican  7124  infcntss  7125  fiint  7128  marypha1lem  7181  wdomen1  7285  wdomen2  7286  unxpwdom2  7297  infdifsn  7352  cnfcom2lem  7399  karden  7560  finnum  7576  cardidm  7587  cardnueq0  7592  carden2a  7594  carden2b  7595  card1  7596  cardsdomel  7602  isinffi  7620  fidomtri2  7622  cardmin2  7626  pr2ne  7630  en2eqpr  7632  infxpenlem  7636  infxpidm2  7639  acnen  7675  acnen2  7677  infpwfien  7684  alephnbtwn2  7694  alephordi  7696  alephsucdom  7701  alephinit  7717  mappwen  7734  finnisoeu  7735  dfac12lem2  7765  dfac12r  7767  uncdadom  7792  cdaen  7794  cda1en  7796  cdacomen  7802  cdaassen  7803  xpcdaen  7804  cdainf  7813  infcda1  7814  pwcda1  7815  onacda  7818  cardacda  7819  cdanum  7820  ficardun  7823  pwsdompw  7825  infdif2  7831  infxp  7836  infmap2  7839  ackbij1lem5  7845  ackbij1b  7860  cflim2  7884  cfss  7886  fin4en1  7930  domfin4  7932  ominf4  7933  isfin4-3  7936  fin23lem25  7945  fin23lem23  7947  fin23lem27  7949  enfin1ai  8005  fin67  8016  isfin7-2  8017  fin1a2lem11  8031  axcc2lem  8057  axcclem  8078  numthcor  8116  carden  8168  sdomsdomcard  8177  alephsuc3  8197  canthnum  8266  canthwe  8268  canthp1lem1  8269  canthp1lem2  8270  canthp1  8271  gchcda1  8273  gchinf  8274  pwfseqlem5  8280  pwxpndom2  8282  pwcdandom  8284  gchcdaidm  8285  gchxpidm  8286  gchhar  8288  gchpwdom  8291  inawinalem  8306  inttsk  8391  tskcard  8398  r1tskina  8399  tskuni  8400  grudomon  8434  hashkf  11333  hashfn  11351  fz1isolem  11393  isercolllem2  12133  summolem2a  12182  summolem2  12183  zsum  12185  isprm2lem  12759  4sqlem11  12996  ramub2  13055  orbsta2  14762  dfod2  14871  sylow2blem1  14925  znhash  16506  hauspwdom  17221  rectbntr0  18331  ovolctb  18843  ovoliunlem1  18855  dyadmbl  18949  derangen  23107  eupafi  23290  carinttar2  25302  finminlem  25630  enf1f1oOLD  25796  eldioph2lem1  26238  pellexlem4  26316  pellexlem5  26317  pellex  26319  isnumbasgrplem3  26669  en2eleq  26780  psgnunilem1  26815  fiuneneq  26912
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265  ax-sep 4142  ax-nul 4150  ax-pow 4187  ax-pr 4213  ax-un 4511
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 938  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-eu 2148  df-mo 2149  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-ral 2549  df-rex 2550  df-rab 2553  df-v 2791  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-pw 3628  df-sn 3647  df-pr 3648  df-op 3650  df-uni 3829  df-br 4025  df-opab 4079  df-id 4308  df-xp 4694  df-rel 4695  df-cnv 4696  df-co 4697  df-dm 4698  df-rn 4699  df-res 4700  df-ima 4701  df-fun 5223  df-fn 5224  df-f 5225  df-f1 5226  df-fo 5227  df-f1o 5228  df-er 6655  df-en 6859
  Copyright terms: Public domain W3C validator