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

Theorem ensym 8235
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 8234 . 2 (𝐴𝐵𝐵𝐴)
21biimpi 207 1 (𝐴𝐵𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   class class class wbr 4837  cen 8183
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-8 2157  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781  ax-sep 4968  ax-nul 4977  ax-pow 5029  ax-pr 5090  ax-un 7173
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-eu 2633  df-mo 2634  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-ral 3097  df-rex 3098  df-rab 3101  df-v 3389  df-dif 3766  df-un 3768  df-in 3770  df-ss 3777  df-nul 4111  df-if 4274  df-pw 4347  df-sn 4365  df-pr 4367  df-op 4371  df-uni 4624  df-br 4838  df-opab 4900  df-id 5213  df-xp 5311  df-rel 5312  df-cnv 5313  df-co 5314  df-dm 5315  df-rn 5316  df-res 5317  df-ima 5318  df-fun 6097  df-fn 6098  df-f 6099  df-f1 6100  df-fo 6101  df-f1o 6102  df-er 7973  df-en 8187
This theorem is referenced by:  ensymi  8236  ensymd  8237  sbthb  8314  domnsym  8319  sdomdomtr  8326  domsdomtr  8328  enen1  8333  enen2  8334  domen1  8335  domen2  8336  sdomen1  8337  sdomen2  8338  domtriord  8339  xpen  8356  pwen  8366  nneneq  8376  php2  8378  php3  8379  ominf  8405  fineqvlem  8407  en1eqsn  8423  dif1en  8426  enp1i  8428  findcard3  8436  isfinite2  8451  nnsdomg  8452  domunfican  8466  infcntss  8467  fiint  8470  wdomen1  8714  wdomen2  8715  unxpwdom2  8726  karden  8999  finnum  9051  carden2b  9070  fidomtri2  9097  cardmin2  9101  pr2ne  9105  en2eleq  9108  infxpenlem  9113  acnen  9153  acnen2  9155  infpwfien  9162  alephordi  9174  alephinit  9195  dfac12lem2  9245  dfac12r  9247  uncdadom  9272  cdacomen  9282  cdainf  9293  pwsdompw  9305  infmap2  9319  ackbij1b  9340  cflim2  9364  fin4en1  9410  domfin4  9412  fin23lem25  9425  fin23lem23  9427  enfin1ai  9485  fin67  9496  isfin7-2  9497  fin1a2lem11  9511  axcc2lem  9537  axcclem  9558  numthcor  9595  carden  9652  sdomsdomcard  9661  canthnum  9750  canthwe  9752  canthp1lem2  9754  canthp1  9755  pwxpndom2  9766  gchcdaidm  9769  gchxpidm  9770  gchpwdom  9771  inawinalem  9790  grudomon  9918  isfinite4  13365  hashfn  13376  ramub2  15929  dfod2  18176  sylow2blem1  18230  znhash  20108  hauspwdom  21512  rectbntr0  22842  ovolctb  23465  dyadmbl  23575  eupthfi  27372  derangen  31471  finminlem  32627  phpreu  33700  pellexlem4  37892  pellexlem5  37893  pellex  37895
  Copyright terms: Public domain W3C validator