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

Theorem ensym 7350
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 7349 . 2  |-  ( A 
~~  B  <->  B  ~~  A )
21biimpi 194 1  |-  ( A 
~~  B  ->  B  ~~  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   class class class wbr 4287    ~~ cen 7299
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-id 4631  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-er 7093  df-en 7303
This theorem is referenced by:  ensymi  7351  ensymd  7352  sbthb  7424  domnsym  7429  sdomdomtr  7436  domsdomtr  7438  enen1  7443  enen2  7444  domen1  7445  domen2  7446  sdomen1  7447  sdomen2  7448  domtriord  7449  xpen  7466  pwen  7476  nneneq  7486  php2  7488  php3  7489  ominf  7517  fineqvlem  7519  en1eqsn  7534  dif1enOLD  7536  dif1en  7537  enp1i  7539  findcard3  7547  isfinite2  7562  nnsdomg  7563  domunfican  7576  infcntss  7577  fiint  7580  wdomen1  7783  wdomen2  7784  unxpwdom2  7795  karden  8094  finnum  8110  carden2b  8129  fidomtri2  8156  cardmin2  8160  pr2ne  8164  en2eleq  8167  infxpenlem  8172  acnen  8215  acnen2  8217  infpwfien  8224  alephordi  8236  alephinit  8257  dfac12lem2  8305  dfac12r  8307  uncdadom  8332  cdacomen  8342  cdainf  8353  pwsdompw  8365  infmap2  8379  ackbij1b  8400  cflim2  8424  fin4en1  8470  domfin4  8472  fin23lem25  8485  fin23lem23  8487  enfin1ai  8545  fin67  8556  isfin7-2  8557  fin1a2lem11  8571  axcc2lem  8597  axcclem  8618  numthcor  8655  carden  8707  sdomsdomcard  8716  canthnum  8808  canthwe  8810  canthp1lem2  8812  canthp1  8813  pwxpndom2  8824  gchcdaidm  8827  gchxpidm  8828  gchpwdom  8829  inawinalem  8848  grudomon  8976  hashfn  12130  isprm2lem  13762  ramub2  14067  dfod2  16056  sylow2blem1  16110  znhash  17966  hauspwdom  19080  rectbntr0  20384  ovolctb  20948  dyadmbl  21055  eupafi  23543  derangen  27012  finminlem  28466  pellexlem4  29126  pellexlem5  29127  pellex  29129
  Copyright terms: Public domain W3C validator