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

Theorem ensymi 8703
Description: Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by NM, 25-Sep-2004.)
Hypothesis
Ref Expression
ensymi.2 𝐴𝐵
Assertion
Ref Expression
ensymi 𝐵𝐴

Proof of Theorem ensymi
StepHypRef Expression
1 ensymi.2 . 2 𝐴𝐵
2 ensym 8702 . 2 (𝐴𝐵𝐵𝐴)
31, 2ax-mp 5 1 𝐵𝐴
Colors of variables: wff setvar class
Syntax hints:   class class class wbr 5069  cen 8646
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-sep 5208  ax-nul 5215  ax-pow 5274  ax-pr 5338  ax-un 7544
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3425  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4456  df-pw 4531  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4836  df-br 5070  df-opab 5132  df-id 5471  df-xp 5574  df-rel 5575  df-cnv 5576  df-co 5577  df-dm 5578  df-rn 5579  df-res 5580  df-ima 5581  df-fun 6402  df-fn 6403  df-f 6404  df-f1 6405  df-fo 6406  df-f1o 6407  df-er 8414  df-en 8650
This theorem is referenced by:  entr2i  8708  entr3i  8709  entr4i  8710  pm54.43  9646  infxpenlem  9656  unsnen  10196  cfpwsdom  10227  tskinf  10412  inar1  10418  gruina  10461  uzenom  13568  znnen  15805  qnnen  15806  rexpen  15821  rucALT  15823  aleph1re  15838  aleph1irr  15839  unben  16494  1stcfb  22373  2ndcredom  22378  hauspwdom  22429  met1stc  23450  ovolctb2  24420  ovolfi  24422  ovoliunlem3  24432  uniiccdif  24506  dyadmbl  24528  mbfimaopnlem  24583  aannenlem3  25254  f1ocnt  30874  dmvlsiga  31840  sigapildsys  31873  omssubadd  32010  carsgclctunlem3  32030  pellex  40407  tr3dom  40867  nnfoctb  42315  nnf1oxpnn  42454  ioonct  42795  caragenunicl  43782  rrx2xpreen  45783  aacllem  46221
  Copyright terms: Public domain W3C validator