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

Theorem ensymd 7356
Description: Symmetry of equinumerosity. Deduction form of ensym 7354. (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 7354 . 2  |-  ( A 
~~  B  ->  B  ~~  A )
31, 2syl 16 1  |-  ( ph  ->  B  ~~  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   class class class wbr 4289    ~~ cen 7303
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2261  df-mo 2262  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-br 4290  df-opab 4348  df-id 4632  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-er 7097  df-en 7307
This theorem is referenced by:  f1imaeng  7365  f1imaen2g  7366  en2sn  7385  xpdom3  7405  omxpen  7409  mapdom2  7478  mapdom3  7479  limensuci  7483  phplem4  7489  php  7491  unxpdom2  7517  sucxpdom  7518  fiint  7584  marypha1lem  7679  infdifsn  7858  cnfcom2lem  7930  cnfcom2lemOLD  7938  cardidm  8125  cardnueq0  8130  carden2a  8132  card1  8134  cardsdomel  8140  isinffi  8158  en2eqpr  8170  infxpenlem  8176  infxpidm2  8179  alephnbtwn2  8238  alephsucdom  8245  mappwen  8278  finnisoeu  8279  cdaen  8338  cda1en  8340  cdaassen  8347  xpcdaen  8348  infcda1  8358  pwcda1  8359  onacda  8362  cardacda  8363  cdanum  8364  ficardun  8367  pwsdompw  8369  infdif2  8375  infxp  8380  ackbij1lem5  8389  cfss  8430  ominf4  8477  isfin4-3  8480  fin23lem27  8493  alephsuc3  8740  canthp1lem1  8815  gchcda1  8819  gchinf  8820  pwfseqlem5  8826  pwcdandom  8830  gchcdaidm  8831  gchxpidm  8832  gchhar  8842  inttsk  8937  tskcard  8944  r1tskina  8945  tskuni  8946  hashkf  12101  fz1isolem  12210  isercolllem2  13139  summolem2a  13188  summolem2  13189  zsum  13191  4sqlem11  14012  mreexexd  14582  orbsta2  15825  psgnunilem1  15992  frlmisfrlm  18236  frlmiscvec  18237  ovoliunlem1  20944  prodmolem2a  27376  prodmolem2  27377  zprod  27379  heicant  28351  mblfinlem1  28353  eldioph2lem1  29023  isnumbasgrplem3  29386  fiuneneq  29487
  Copyright terms: Public domain W3C validator