Theorem ensymd 8007

Description: Symmetry of equinumerosity. Deduction form of ensym 8005. (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

Step	Hyp	Ref	Expression
1		ensymd.1	. 2 |- ( ph -> A ~~ B )
2		ensym 8005	. 2 |- ( A ~~ B -> B ~~ A )
3	1, 2	syl 17	1 |- ( ph -> B ~~ A )

Syntax hints:   -> wi 4   class class class wbr 4653   ~~ cen 7952

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-er 7742  df-en 7956

This theorem is referenced by:  f1imaeng  8016  f1imaen2g  8017  en2sn  8037  xpdom3  8058  omxpen  8062  mapdom2  8131  mapdom3  8132  limensuci  8136  phplem4  8142  php  8144  unxpdom2  8168  sucxpdom  8169  fiint  8237  marypha1lem  8339  infdifsn  8554  cnfcom2lem  8598  cardidm  8785  cardnueq0  8790  carden2a  8792  card1  8794  cardsdomel  8800  isinffi  8818  en2eqpr  8830  infxpenlem  8836  infxpidm2  8840  alephnbtwn2  8895  alephsucdom  8902  mappwen  8935  finnisoeu  8936  cdaen  8995  cda1en  8997  cdaassen  9004  xpcdaen  9005  infcda1  9015  pwcda1  9016  onacda  9019  cardacda  9020  cdanum  9021  ficardun  9024  pwsdompw  9026  infdif2  9032  infxp  9037  ackbij1lem5  9046  cfss  9087  ominf4  9134  isfin4-3  9137  fin23lem27  9150  alephsuc3  9402  canthp1lem1  9474  gchcda1  9478  gchinf  9479  pwfseqlem5  9485  pwcdandom  9489  gchcdaidm  9490  gchxpidm  9491  gchhar  9501  inttsk  9596  tskcard  9603  r1tskina  9604  tskuni  9605  hashkf  13119  fz1isolem  13245  isercolllem2  14396  summolem2a  14446  summolem2  14447  zsum  14449  prodmolem2a  14664  prodmolem2  14665  zprod  14667  4sqlem11  15659  mreexexd  16308  mreexexdOLD  16309  orbsta2  17747  psgnunilem1  17913  frlmisfrlm  20187  frlmiscvec  20188  ovoliunlem1  23270  rabfodom  29344  padct  29497  lindsdom  33403  matunitlindflem2  33406  heicant  33444  mblfinlem1  33446  eldioph2lem1  37323  isnumbasgrplem3  37675  fiuneneq  37775  enrelmap  38291  enmappw  38293