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

Theorem ensymd 7630
Description: Symmetry of equinumerosity. Deduction form of ensym 7628. (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 7628 . 2  |-  ( A 
~~  B  ->  B  ~~  A )
31, 2syl 17 1  |-  ( ph  ->  B  ~~  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   class class class wbr 4423    ~~ cen 7577
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6597
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-br 4424  df-opab 4483  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-er 7374  df-en 7581
This theorem is referenced by:  f1imaeng  7639  f1imaen2g  7640  en2sn  7659  xpdom3  7679  omxpen  7683  mapdom2  7752  mapdom3  7753  limensuci  7757  phplem4  7763  php  7765  unxpdom2  7789  sucxpdom  7790  fiint  7857  marypha1lem  7956  infdifsn  8170  cnfcom2lem  8214  cardidm  8401  cardnueq0  8406  carden2a  8408  card1  8410  cardsdomel  8416  isinffi  8434  en2eqpr  8446  infxpenlem  8452  infxpidm2  8455  alephnbtwn2  8510  alephsucdom  8517  mappwen  8550  finnisoeu  8551  cdaen  8610  cda1en  8612  cdaassen  8619  xpcdaen  8620  infcda1  8630  pwcda1  8631  onacda  8634  cardacda  8635  cdanum  8636  ficardun  8639  pwsdompw  8641  infdif2  8647  infxp  8652  ackbij1lem5  8661  cfss  8702  ominf4  8749  isfin4-3  8752  fin23lem27  8765  alephsuc3  9012  canthp1lem1  9084  gchcda1  9088  gchinf  9089  pwfseqlem5  9095  pwcdandom  9099  gchcdaidm  9100  gchxpidm  9101  gchhar  9111  inttsk  9206  tskcard  9213  r1tskina  9214  tskuni  9215  hashkf  12523  fz1isolem  12628  isercolllem2  13728  summolem2a  13780  summolem2  13781  zsum  13783  prodmolem2a  13987  prodmolem2  13988  zprod  13990  4sqlem11  14898  mreexexd  15553  orbsta2  16967  psgnunilem1  17133  frlmisfrlm  19404  frlmiscvec  19405  ovoliunlem1  22453  rabfodom  28139  padct  28313  heicant  31939  mblfinlem1  31941  eldioph2lem1  35571  isnumbasgrplem3  35934  fiuneneq  36041
  Copyright terms: Public domain W3C validator