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

Theorem ensym 7644
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 7643 . 2  |-  ( A 
~~  B  <->  B  ~~  A )
21biimpi 199 1  |-  ( A 
~~  B  ->  B  ~~  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   class class class wbr 4416    ~~ cen 7592
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4417  df-opab 4476  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-er 7389  df-en 7596
This theorem is referenced by:  ensymi  7645  ensymd  7646  sbthb  7719  domnsym  7724  sdomdomtr  7731  domsdomtr  7733  enen1  7738  enen2  7739  domen1  7740  domen2  7741  sdomen1  7742  sdomen2  7743  domtriord  7744  xpen  7761  pwen  7771  nneneq  7781  php2  7783  php3  7784  ominf  7810  fineqvlem  7812  en1eqsn  7827  dif1en  7830  enp1i  7832  findcard3  7840  isfinite2  7855  nnsdomg  7856  domunfican  7870  infcntss  7871  fiint  7874  wdomen1  8117  wdomen2  8118  unxpwdom2  8129  karden  8392  finnum  8408  carden2b  8427  fidomtri2  8454  cardmin2  8458  pr2ne  8462  en2eleq  8465  infxpenlem  8470  acnen  8510  acnen2  8512  infpwfien  8519  alephordi  8531  alephinit  8552  dfac12lem2  8600  dfac12r  8602  uncdadom  8627  cdacomen  8637  cdainf  8648  pwsdompw  8660  infmap2  8674  ackbij1b  8695  cflim2  8719  fin4en1  8765  domfin4  8767  fin23lem25  8780  fin23lem23  8782  enfin1ai  8840  fin67  8851  isfin7-2  8852  fin1a2lem11  8866  axcc2lem  8892  axcclem  8913  numthcor  8950  carden  9002  sdomsdomcard  9011  canthnum  9100  canthwe  9102  canthp1lem2  9104  canthp1  9105  pwxpndom2  9116  gchcdaidm  9119  gchxpidm  9120  gchpwdom  9121  inawinalem  9140  grudomon  9268  isfinite4  12575  hashfn  12586  isprm2lem  14680  ramub2  15020  dfod2  17264  sylow2blem1  17321  znhash  19178  hauspwdom  20565  rectbntr0  21899  ovolctb  22492  dyadmbl  22607  eupafi  25748  derangen  29944  finminlem  31023  phpreu  31974  pellexlem4  35721  pellexlem5  35722  pellex  35724
  Copyright terms: Public domain W3C validator