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

Theorem ensym 7616
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 7615 . 2  |-  ( A 
~~  B  <->  B  ~~  A )
21biimpi 197 1  |-  ( A 
~~  B  ->  B  ~~  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   class class class wbr 4417    ~~ cen 7565
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4539  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6588
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-ral 2778  df-rex 2779  df-rab 2782  df-v 3080  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4214  df-br 4418  df-opab 4476  df-id 4760  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-fun 5594  df-fn 5595  df-f 5596  df-f1 5597  df-fo 5598  df-f1o 5599  df-er 7362  df-en 7569
This theorem is referenced by:  ensymi  7617  ensymd  7618  sbthb  7690  domnsym  7695  sdomdomtr  7702  domsdomtr  7704  enen1  7709  enen2  7710  domen1  7711  domen2  7712  sdomen1  7713  sdomen2  7714  domtriord  7715  xpen  7732  pwen  7742  nneneq  7752  php2  7754  php3  7755  ominf  7781  fineqvlem  7783  en1eqsn  7798  dif1en  7801  enp1i  7803  findcard3  7811  isfinite2  7826  nnsdomg  7827  domunfican  7841  infcntss  7842  fiint  7845  wdomen1  8082  wdomen2  8083  unxpwdom2  8094  karden  8356  finnum  8372  carden2b  8391  fidomtri2  8418  cardmin2  8422  pr2ne  8426  en2eleq  8429  infxpenlem  8434  acnen  8473  acnen2  8475  infpwfien  8482  alephordi  8494  alephinit  8515  dfac12lem2  8563  dfac12r  8565  uncdadom  8590  cdacomen  8600  cdainf  8611  pwsdompw  8623  infmap2  8637  ackbij1b  8658  cflim2  8682  fin4en1  8728  domfin4  8730  fin23lem25  8743  fin23lem23  8745  enfin1ai  8803  fin67  8814  isfin7-2  8815  fin1a2lem11  8829  axcc2lem  8855  axcclem  8876  numthcor  8913  carden  8965  sdomsdomcard  8974  canthnum  9063  canthwe  9065  canthp1lem2  9067  canthp1  9068  pwxpndom2  9079  gchcdaidm  9082  gchxpidm  9083  gchpwdom  9084  inawinalem  9103  grudomon  9231  isfinite4  12529  hashfn  12540  isprm2lem  14591  ramub2  14923  dfod2  17146  sylow2blem1  17200  znhash  19053  hauspwdom  20440  rectbntr0  21754  ovolctb  22317  dyadmbl  22432  eupafi  25541  derangen  29680  finminlem  30756  phpreu  31633  pellexlem4  35386  pellexlem5  35387  pellex  35389
  Copyright terms: Public domain W3C validator