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

Theorem ensym 7123
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 7122 . 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 4180    ~~ cen 7073
This theorem is referenced by:  ensymi  7124  ensymd  7125  sbthb  7195  domnsym  7200  sdomdomtr  7207  domsdomtr  7209  enen1  7214  enen2  7215  domen1  7216  domen2  7217  sdomen1  7218  sdomen2  7219  domtriord  7220  xpen  7237  pwen  7247  nneneq  7257  php2  7259  php3  7260  ominf  7288  fineqvlem  7290  en1eqsn  7305  dif1enOLD  7307  dif1en  7308  enp1i  7310  findcard3  7317  isfinite2  7332  nnsdomg  7333  domunfican  7346  infcntss  7347  fiint  7350  wdomen1  7508  wdomen2  7509  unxpwdom2  7520  karden  7783  finnum  7799  carden2b  7818  fidomtri2  7845  cardmin2  7849  pr2ne  7853  infxpenlem  7859  acnen  7898  acnen2  7900  infpwfien  7907  alephordi  7919  alephinit  7940  dfac12lem2  7988  dfac12r  7990  uncdadom  8015  cdacomen  8025  cdainf  8036  pwsdompw  8048  infmap2  8062  ackbij1b  8083  cflim2  8107  fin4en1  8153  domfin4  8155  fin23lem25  8168  fin23lem23  8170  enfin1ai  8228  fin67  8239  isfin7-2  8240  fin1a2lem11  8254  axcc2lem  8280  axcclem  8301  numthcor  8338  carden  8390  sdomsdomcard  8399  canthnum  8488  canthwe  8490  canthp1lem2  8492  canthp1  8493  pwxpndom2  8504  gchcdaidm  8507  gchxpidm  8508  gchpwdom  8513  inawinalem  8528  grudomon  8656  hashfn  11612  isprm2lem  13049  ramub2  13345  dfod2  15163  sylow2blem1  15217  znhash  16802  hauspwdom  17525  rectbntr0  18824  ovolctb  19347  dyadmbl  19453  eupafi  21654  derangen  24819  finminlem  26219  pellexlem4  26793  pellexlem5  26794  pellex  26796  en2eleq  27257
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 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-sep 4298  ax-nul 4306  ax-pow 4345  ax-pr 4371  ax-un 4668
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 2266  df-mo 2267  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-ral 2679  df-rex 2680  df-rab 2683  df-v 2926  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-nul 3597  df-if 3708  df-pw 3769  df-sn 3788  df-pr 3789  df-op 3791  df-uni 3984  df-br 4181  df-opab 4235  df-id 4466  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 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428  df-er 6872  df-en 7077
  Copyright terms: Public domain W3C validator