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

Theorem ensym 7092
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 7091 . 2  |-  ( A 
~~  B  <->  B  ~~  A )
21biimpi 187 1  |-  ( A 
~~  B  ->  B  ~~  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4   class class class wbr 4153    ~~ cen 7042
This theorem is referenced by:  ensymi  7093  ensymd  7094  sbthb  7164  domnsym  7169  sdomdomtr  7176  domsdomtr  7178  enen1  7183  enen2  7184  domen1  7185  domen2  7186  sdomen1  7187  sdomen2  7188  domtriord  7189  xpen  7206  pwen  7216  nneneq  7226  php2  7228  php3  7229  ominf  7257  fineqvlem  7259  en1eqsn  7274  dif1enOLD  7276  dif1en  7277  enp1i  7279  findcard3  7286  isfinite2  7301  nnsdomg  7302  domunfican  7315  infcntss  7316  fiint  7319  wdomen1  7477  wdomen2  7478  unxpwdom2  7489  karden  7752  finnum  7768  carden2b  7787  fidomtri2  7814  cardmin2  7818  pr2ne  7822  infxpenlem  7828  acnen  7867  acnen2  7869  infpwfien  7876  alephordi  7888  alephinit  7909  dfac12lem2  7957  dfac12r  7959  uncdadom  7984  cdacomen  7994  cdainf  8005  pwsdompw  8017  infmap2  8031  ackbij1b  8052  cflim2  8076  fin4en1  8122  domfin4  8124  fin23lem25  8137  fin23lem23  8139  enfin1ai  8197  fin67  8208  isfin7-2  8209  fin1a2lem11  8223  axcc2lem  8249  axcclem  8270  numthcor  8307  carden  8359  sdomsdomcard  8368  canthnum  8457  canthwe  8459  canthp1lem2  8461  canthp1  8462  pwxpndom2  8473  gchcdaidm  8476  gchxpidm  8477  gchpwdom  8482  inawinalem  8497  grudomon  8625  hashfn  11576  isprm2lem  13013  ramub2  13309  dfod2  15127  sylow2blem1  15181  znhash  16762  hauspwdom  17485  rectbntr0  18734  ovolctb  19253  dyadmbl  19359  eupafi  21541  derangen  24637  finminlem  26012  pellexlem4  26586  pellexlem5  26587  pellex  26589  en2eleq  27050
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-sep 4271  ax-nul 4279  ax-pow 4318  ax-pr 4344  ax-un 4641
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2242  df-mo 2243  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-ral 2654  df-rex 2655  df-rab 2658  df-v 2901  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-pw 3744  df-sn 3763  df-pr 3764  df-op 3766  df-uni 3958  df-br 4154  df-opab 4208  df-id 4439  df-xp 4824  df-rel 4825  df-cnv 4826  df-co 4827  df-dm 4828  df-rn 4829  df-res 4830  df-ima 4831  df-fun 5396  df-fn 5397  df-f 5398  df-f1 5399  df-fo 5400  df-f1o 5401  df-er 6841  df-en 7046
  Copyright terms: Public domain W3C validator