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

Theorem ensymd 7160
Description: Symmetry of equinumerosity. Deduction form of ensym 7158. (Contributed by David Moews, 1-May-2017.)
Hypothesis
Ref Expression
ensymd.1  |-  ( ph  ->  A  ~~  B )
Assertion
Ref Expression
ensymd  |-  ( ph  ->  B  ~~  A )

Proof of Theorem ensymd
StepHypRef Expression
1 ensymd.1 . 2  |-  ( ph  ->  A  ~~  B )
2 ensym 7158 . 2  |-  ( A 
~~  B  ->  B  ~~  A )
31, 2syl 16 1  |-  ( ph  ->  B  ~~  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4   class class class wbr 4214    ~~ cen 7108
This theorem is referenced by:  f1imaeng  7169  f1imaen2g  7170  en2sn  7188  xpdom3  7208  omxpen  7212  mapdom2  7280  mapdom3  7281  limensuci  7285  phplem4  7291  php  7293  unxpdom2  7319  sucxpdom  7320  fiint  7385  marypha1lem  7440  infdifsn  7613  cnfcom2lem  7660  cardidm  7848  cardnueq0  7853  carden2a  7855  card1  7857  cardsdomel  7863  isinffi  7881  en2eqpr  7893  infxpenlem  7897  infxpidm2  7900  alephnbtwn2  7955  alephsucdom  7962  mappwen  7995  finnisoeu  7996  cdaen  8055  cda1en  8057  cdaassen  8064  xpcdaen  8065  infcda1  8075  pwcda1  8076  onacda  8079  cardacda  8080  cdanum  8081  ficardun  8084  pwsdompw  8086  infdif2  8092  infxp  8097  ackbij1lem5  8106  cfss  8147  ominf4  8194  isfin4-3  8197  fin23lem27  8210  alephsuc3  8457  canthp1lem1  8529  gchcda1  8533  gchinf  8534  pwfseqlem5  8540  pwcdandom  8544  gchcdaidm  8545  gchxpidm  8546  gchhar  8548  inttsk  8651  tskcard  8658  r1tskina  8659  tskuni  8660  hashkf  11622  fz1isolem  11712  isercolllem2  12461  summolem2a  12511  summolem2  12512  zsum  12514  4sqlem11  13325  mreexexd  13875  orbsta2  15093  ovoliunlem1  19400  prodmolem2a  25262  prodmolem2  25263  zprod  25265  mblfinlem1  26245  eldioph2lem1  26820  isnumbasgrplem3  27249  psgnunilem1  27395  fiuneneq  27492
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4332  ax-nul 4340  ax-pow 4379  ax-pr 4405  ax-un 4703
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4215  df-opab 4269  df-id 4500  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-fun 5458  df-fn 5459  df-f 5460  df-f1 5461  df-fo 5462  df-f1o 5463  df-er 6907  df-en 7112
  Copyright terms: Public domain W3C validator