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

Theorem ensym 6796
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 6795 . 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 3920    ~~ cen 6746
This theorem is referenced by:  ensymi  6797  f1imaeng  6806  f1imaen2g  6807  en2sn  6825  xpdom3  6845  omxpen  6849  sbthb  6867  domnsym  6872  sdomdomtr  6879  domsdomtr  6881  enen1  6886  enen2  6887  domen1  6888  domen2  6889  sdomen1  6890  sdomen2  6891  domtriord  6892  xpen  6909  mapdom2  6917  mapdom3  6918  pwen  6919  limensuci  6922  phplem4  6928  nneneq  6929  php  6930  php2  6931  php3  6932  unxpdom2  6956  sucxpdom  6957  ominf  6960  fineqvlem  6962  en1eqsn  6973  dif1enOLD  6975  dif1en  6976  enp1i  6978  findcard3  6985  isfinite2  7000  nnsdomg  7001  domunfican  7014  infcntss  7015  fiint  7018  marypha1lem  7070  wdomen1  7174  wdomen2  7175  unxpwdom2  7186  infdifsn  7241  cnfcom2lem  7288  karden  7449  finnum  7465  cardidm  7476  cardnueq0  7481  carden2a  7483  carden2b  7484  card1  7485  cardsdomel  7491  isinffi  7509  fidomtri2  7511  cardmin2  7515  pr2ne  7519  en2eqpr  7521  infxpenlem  7525  infxpidm2  7528  acnen  7564  acnen2  7566  infpwfien  7573  alephnbtwn2  7583  alephordi  7585  alephsucdom  7590  alephinit  7606  mappwen  7623  finnisoeu  7624  dfac12lem2  7654  dfac12r  7656  uncdadom  7681  cdaen  7683  cda1en  7685  cdacomen  7691  cdaassen  7692  xpcdaen  7693  cdainf  7702  infcda1  7703  pwcda1  7704  onacda  7707  cardacda  7708  cdanum  7709  ficardun  7712  pwsdompw  7714  infdif2  7720  infxp  7725  infmap2  7728  ackbij1lem5  7734  ackbij1b  7749  cflim2  7773  cfss  7775  fin4en1  7819  domfin4  7821  ominf4  7822  isfin4-3  7825  fin23lem25  7834  fin23lem23  7836  fin23lem27  7838  enfin1ai  7894  fin67  7905  isfin7-2  7906  fin1a2lem11  7920  axcc2lem  7946  axcclem  7967  numthcor  8005  carden  8055  sdomsdomcard  8064  alephsuc3  8082  canthnum  8151  canthwe  8153  canthp1lem1  8154  canthp1lem2  8155  canthp1  8156  gchcda1  8158  gchinf  8159  pwfseqlem5  8165  pwxpndom2  8167  pwcdandom  8169  gchcdaidm  8170  gchxpidm  8171  gchhar  8173  gchpwdom  8176  inawinalem  8191  inttsk  8276  tskcard  8283  r1tskina  8284  tskuni  8285  grudomon  8319  hashkf  11217  hashfn  11235  fz1isolem  11276  isercolllem2  12016  summolem2a  12065  summolem2  12066  zsum  12068  isprm2lem  12639  4sqlem11  12876  ramub2  12935  orbsta2  14603  dfod2  14712  sylow2blem1  14766  znhash  16344  hauspwdom  17059  rectbntr0  18169  ovolctb  18681  ovoliunlem1  18693  dyadmbl  18787  derangen  22874  eupafi  23057  carinttar2  25069  finminlem  25397  enf1f1oOLD  25563  eldioph2lem1  26005  pellexlem4  26083  pellexlem5  26084  pellex  26086  isnumbasgrplem3  26436  en2eleq  26547  psgnunilem1  26582  fiuneneq  26679
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-sep 4038  ax-nul 4046  ax-pow 4082  ax-pr 4108  ax-un 4403
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-eu 2118  df-mo 2119  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-ral 2513  df-rex 2514  df-rab 2516  df-v 2729  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-nul 3363  df-if 3471  df-pw 3532  df-sn 3550  df-pr 3551  df-op 3553  df-uni 3728  df-br 3921  df-opab 3975  df-id 4202  df-xp 4594  df-rel 4595  df-cnv 4596  df-co 4597  df-dm 4598  df-rn 4599  df-res 4600  df-ima 4601  df-fun 4602  df-fn 4603  df-f 4604  df-f1 4605  df-fo 4606  df-f1o 4607  df-er 6546  df-en 6750
  Copyright terms: Public domain W3C validator