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

Theorem ensym 7557
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 7556 . 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 4439    ~~ cen 7506
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-er 7303  df-en 7510
This theorem is referenced by:  ensymi  7558  ensymd  7559  sbthb  7631  domnsym  7636  sdomdomtr  7643  domsdomtr  7645  enen1  7650  enen2  7651  domen1  7652  domen2  7653  sdomen1  7654  sdomen2  7655  domtriord  7656  xpen  7673  pwen  7683  nneneq  7693  php2  7695  php3  7696  ominf  7725  fineqvlem  7727  en1eqsn  7742  dif1en  7745  enp1i  7747  findcard3  7755  isfinite2  7770  nnsdomg  7771  domunfican  7785  infcntss  7786  fiint  7789  wdomen1  7994  wdomen2  7995  unxpwdom2  8006  karden  8304  finnum  8320  carden2b  8339  fidomtri2  8366  cardmin2  8370  pr2ne  8374  en2eleq  8377  infxpenlem  8382  acnen  8425  acnen2  8427  infpwfien  8434  alephordi  8446  alephinit  8467  dfac12lem2  8515  dfac12r  8517  uncdadom  8542  cdacomen  8552  cdainf  8563  pwsdompw  8575  infmap2  8589  ackbij1b  8610  cflim2  8634  fin4en1  8680  domfin4  8682  fin23lem25  8695  fin23lem23  8697  enfin1ai  8755  fin67  8766  isfin7-2  8767  fin1a2lem11  8781  axcc2lem  8807  axcclem  8828  numthcor  8865  carden  8917  sdomsdomcard  8926  canthnum  9016  canthwe  9018  canthp1lem2  9020  canthp1  9021  pwxpndom2  9032  gchcdaidm  9035  gchxpidm  9036  gchpwdom  9037  inawinalem  9056  grudomon  9184  isfinite4  12415  hashfn  12426  isprm2lem  14308  ramub2  14616  dfod2  16785  sylow2blem1  16839  znhash  18770  hauspwdom  20168  rectbntr0  21503  ovolctb  22067  dyadmbl  22175  eupafi  25173  derangen  28880  finminlem  30376  pellexlem4  31007  pellexlem5  31008  pellex  31010
  Copyright terms: Public domain W3C validator