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

Theorem ensym 6910
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 6909 . 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 4023    ~~ cen 6860
This theorem is referenced by:  ensymi  6911  ensymd  6912  f1imaeng  6921  f1imaen2g  6922  en2sn  6940  xpdom3  6960  omxpen  6964  sbthb  6982  domnsym  6987  sdomdomtr  6994  domsdomtr  6996  enen1  7001  enen2  7002  domen1  7003  domen2  7004  sdomen1  7005  sdomen2  7006  domtriord  7007  xpen  7024  mapdom2  7032  mapdom3  7033  pwen  7034  limensuci  7037  phplem4  7043  nneneq  7044  php  7045  php2  7046  php3  7047  unxpdom2  7071  sucxpdom  7072  ominf  7075  fineqvlem  7077  en1eqsn  7088  dif1enOLD  7090  dif1en  7091  enp1i  7093  findcard3  7100  isfinite2  7115  nnsdomg  7116  domunfican  7129  infcntss  7130  fiint  7133  marypha1lem  7186  wdomen1  7290  wdomen2  7291  unxpwdom2  7302  infdifsn  7357  cnfcom2lem  7404  karden  7565  finnum  7581  cardidm  7592  cardnueq0  7597  carden2a  7599  carden2b  7600  card1  7601  cardsdomel  7607  isinffi  7625  fidomtri2  7627  cardmin2  7631  pr2ne  7635  en2eqpr  7637  infxpenlem  7641  infxpidm2  7644  acnen  7680  acnen2  7682  infpwfien  7689  alephnbtwn2  7699  alephordi  7701  alephsucdom  7706  alephinit  7722  mappwen  7739  finnisoeu  7740  dfac12lem2  7770  dfac12r  7772  uncdadom  7797  cdaen  7799  cda1en  7801  cdacomen  7807  cdaassen  7808  xpcdaen  7809  cdainf  7818  infcda1  7819  pwcda1  7820  onacda  7823  cardacda  7824  cdanum  7825  ficardun  7828  pwsdompw  7830  infdif2  7836  infxp  7841  infmap2  7844  ackbij1lem5  7850  ackbij1b  7865  cflim2  7889  cfss  7891  fin4en1  7935  domfin4  7937  ominf4  7938  isfin4-3  7941  fin23lem25  7950  fin23lem23  7952  fin23lem27  7954  enfin1ai  8010  fin67  8021  isfin7-2  8022  fin1a2lem11  8036  axcc2lem  8062  axcclem  8083  numthcor  8121  carden  8173  sdomsdomcard  8182  alephsuc3  8202  canthnum  8271  canthwe  8273  canthp1lem1  8274  canthp1lem2  8275  canthp1  8276  gchcda1  8278  gchinf  8279  pwfseqlem5  8285  pwxpndom2  8287  pwcdandom  8289  gchcdaidm  8290  gchxpidm  8291  gchhar  8293  gchpwdom  8296  inawinalem  8311  inttsk  8396  tskcard  8403  r1tskina  8404  tskuni  8405  grudomon  8439  hashkf  11339  hashfn  11357  fz1isolem  11399  isercolllem2  12139  summolem2a  12188  summolem2  12189  zsum  12191  isprm2lem  12765  4sqlem11  13002  ramub2  13061  orbsta2  14768  dfod2  14877  sylow2blem1  14931  znhash  16512  hauspwdom  17227  rectbntr0  18337  ovolctb  18849  ovoliunlem1  18861  dyadmbl  18955  derangen  23703  eupafi  23886  carinttar2  25903  finminlem  26231  enf1f1oOLD  26397  eldioph2lem1  26839  pellexlem4  26917  pellexlem5  26918  pellex  26920  isnumbasgrplem3  27270  en2eleq  27381  psgnunilem1  27416  fiuneneq  27513
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-er 6660  df-en 6864
  Copyright terms: Public domain W3C validator