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

Theorem ensym 6926
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 6925 . 2  |-  ( A 
~~  B  <->  B  ~~  A )
21biimpi 186 1  |-  ( A 
~~  B  ->  B  ~~  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4   class class class wbr 4039    ~~ cen 6876
This theorem is referenced by:  ensymi  6927  ensymd  6928  f1imaeng  6937  f1imaen2g  6938  en2sn  6956  xpdom3  6976  omxpen  6980  sbthb  6998  domnsym  7003  sdomdomtr  7010  domsdomtr  7012  enen1  7017  enen2  7018  domen1  7019  domen2  7020  sdomen1  7021  sdomen2  7022  domtriord  7023  xpen  7040  mapdom2  7048  mapdom3  7049  pwen  7050  limensuci  7053  phplem4  7059  nneneq  7060  php  7061  php2  7062  php3  7063  unxpdom2  7087  sucxpdom  7088  ominf  7091  fineqvlem  7093  en1eqsn  7104  dif1enOLD  7106  dif1en  7107  enp1i  7109  findcard3  7116  isfinite2  7131  nnsdomg  7132  domunfican  7145  infcntss  7146  fiint  7149  marypha1lem  7202  wdomen1  7306  wdomen2  7307  unxpwdom2  7318  infdifsn  7373  cnfcom2lem  7420  karden  7581  finnum  7597  cardidm  7608  cardnueq0  7613  carden2a  7615  carden2b  7616  card1  7617  cardsdomel  7623  isinffi  7641  fidomtri2  7643  cardmin2  7647  pr2ne  7651  en2eqpr  7653  infxpenlem  7657  infxpidm2  7660  acnen  7696  acnen2  7698  infpwfien  7705  alephnbtwn2  7715  alephordi  7717  alephsucdom  7722  alephinit  7738  mappwen  7755  finnisoeu  7756  dfac12lem2  7786  dfac12r  7788  uncdadom  7813  cdaen  7815  cda1en  7817  cdacomen  7823  cdaassen  7824  xpcdaen  7825  cdainf  7834  infcda1  7835  pwcda1  7836  onacda  7839  cardacda  7840  cdanum  7841  ficardun  7844  pwsdompw  7846  infdif2  7852  infxp  7857  infmap2  7860  ackbij1lem5  7866  ackbij1b  7881  cflim2  7905  cfss  7907  fin4en1  7951  domfin4  7953  ominf4  7954  isfin4-3  7957  fin23lem25  7966  fin23lem23  7968  fin23lem27  7970  enfin1ai  8026  fin67  8037  isfin7-2  8038  fin1a2lem11  8052  axcc2lem  8078  axcclem  8099  numthcor  8137  carden  8189  sdomsdomcard  8198  alephsuc3  8218  canthnum  8287  canthwe  8289  canthp1lem1  8290  canthp1lem2  8291  canthp1  8292  gchcda1  8294  gchinf  8295  pwfseqlem5  8301  pwxpndom2  8303  pwcdandom  8305  gchcdaidm  8306  gchxpidm  8307  gchhar  8309  gchpwdom  8312  inawinalem  8327  inttsk  8412  tskcard  8419  r1tskina  8420  tskuni  8421  grudomon  8455  hashkf  11355  hashfn  11373  fz1isolem  11415  isercolllem2  12155  summolem2a  12204  summolem2  12205  zsum  12207  isprm2lem  12781  4sqlem11  13018  ramub2  13077  orbsta2  14784  dfod2  14893  sylow2blem1  14947  znhash  16528  hauspwdom  17243  rectbntr0  18353  ovolctb  18865  ovoliunlem1  18877  dyadmbl  18971  derangen  23718  eupafi  23901  carinttar2  26006  finminlem  26334  enf1f1oOLD  26500  eldioph2lem1  26942  pellexlem4  27020  pellexlem5  27021  pellex  27023  isnumbasgrplem3  27373  en2eleq  27484  psgnunilem1  27519  fiuneneq  27616
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230  ax-un 4528
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-opab 4094  df-id 4325  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-er 6676  df-en 6880
  Copyright terms: Public domain W3C validator