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

Theorem ensym 7891
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 (𝐴𝐵𝐵𝐴)

Proof of Theorem ensym
StepHypRef Expression
1 ensymb 7890 . 2 (𝐴𝐵𝐵𝐴)
21biimpi 205 1 (𝐴𝐵𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   class class class wbr 4583  cen 7838
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-er 7629  df-en 7842
This theorem is referenced by:  ensymi  7892  ensymd  7893  sbthb  7966  domnsym  7971  sdomdomtr  7978  domsdomtr  7980  enen1  7985  enen2  7986  domen1  7987  domen2  7988  sdomen1  7989  sdomen2  7990  domtriord  7991  xpen  8008  pwen  8018  nneneq  8028  php2  8030  php3  8031  ominf  8057  fineqvlem  8059  en1eqsn  8075  dif1en  8078  enp1i  8080  findcard3  8088  isfinite2  8103  nnsdomg  8104  domunfican  8118  infcntss  8119  fiint  8122  wdomen1  8364  wdomen2  8365  unxpwdom2  8376  karden  8641  finnum  8657  carden2b  8676  fidomtri2  8703  cardmin2  8707  pr2ne  8711  en2eleq  8714  infxpenlem  8719  acnen  8759  acnen2  8761  infpwfien  8768  alephordi  8780  alephinit  8801  dfac12lem2  8849  dfac12r  8851  uncdadom  8876  cdacomen  8886  cdainf  8897  pwsdompw  8909  infmap2  8923  ackbij1b  8944  cflim2  8968  fin4en1  9014  domfin4  9016  fin23lem25  9029  fin23lem23  9031  enfin1ai  9089  fin67  9100  isfin7-2  9101  fin1a2lem11  9115  axcc2lem  9141  axcclem  9162  numthcor  9199  carden  9252  sdomsdomcard  9261  canthnum  9350  canthwe  9352  canthp1lem2  9354  canthp1  9355  pwxpndom2  9366  gchcdaidm  9369  gchxpidm  9370  gchpwdom  9371  inawinalem  9390  grudomon  9518  isfinite4  13014  hashfn  13025  isprm2lem  15232  ramub2  15556  dfod2  17804  sylow2blem1  17858  znhash  19726  hauspwdom  21114  rectbntr0  22443  ovolctb  23065  dyadmbl  23174  eupafi  26498  derangen  30408  finminlem  31482  phpreu  32563  pellexlem4  36414  pellexlem5  36415  pellex  36417  eupthfi  41373
  Copyright terms: Public domain W3C validator