Theorem ensymd 8619

Description: Symmetry of equinumerosity. Deduction form of ensym 8617. (Contributed by David Moews, 1-May-2017.)

Hypothesis

Ref	Expression
ensymd.1	⊢ (𝜑 → 𝐴 ≈ 𝐵)

Assertion

Ref	Expression
ensymd	⊢ (𝜑 → 𝐵 ≈ 𝐴)

Proof of Theorem ensymd

Step	Hyp	Ref	Expression
1		ensymd.1	. 2 ⊢ (𝜑 → 𝐴 ≈ 𝐵)
2		ensym 8617	. 2 ⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐵 ≈ 𝐴)

Syntax hints:   → wi 4   class class class wbr 5040   ≈ cen 8565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2711  ax-sep 5177  ax-nul 5184  ax-pow 5242  ax-pr 5306  ax-un 7492

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2541  df-eu 2571  df-clab 2718  df-cleq 2731  df-clel 2812  df-nfc 2882  df-ral 3059  df-rex 3060  df-rab 3063  df-v 3402  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4222  df-if 4425  df-pw 4500  df-sn 4527  df-pr 4529  df-op 4533  df-uni 4807  df-br 5041  df-opab 5103  df-id 5439  df-xp 5541  df-rel 5542  df-cnv 5543  df-co 5544  df-dm 5545  df-rn 5546  df-res 5547  df-ima 5548  df-fun 6352  df-fn 6353  df-f 6354  df-f1 6355  df-fo 6356  df-f1o 6357  df-er 8333  df-en 8569

This theorem is referenced by:  f1imaeng  8628  f1imaen2g  8629  en2snOLD  8654  xpdom3  8677  omxpen  8681  mapdom2  8751  mapdom3  8752  limensuci  8756  phplem4  8762  php  8764  unxpdom2  8818  sucxpdom  8819  fiint  8882  marypha1lem  8983  infdifsn  9206  cnfcom2lem  9250  cardidm  9474  cardnueq0  9479  carden2a  9481  card1  9483  cardsdomel  9489  isinffi  9507  en2eqpr  9520  infxpenlem  9526  infxpidm2  9530  alephnbtwn2  9585  alephsucdom  9592  mappwen  9625  finnisoeu  9626  djuen  9682  dju1en  9684  djuassen  9691  xpdjuen  9692  infdju1  9702  pwdju1  9703  onadju  9706  cardadju  9707  djunum  9708  nnadju  9710  ficardadju  9712  ficardun  9713  ficardunOLD  9714  pwsdompw  9717  infdif2  9723  infxp  9728  ackbij1lem5  9737  cfss  9778  ominf4  9825  isfin4p1  9828  fin23lem27  9841  alephsuc3  10093  canthp1lem1  10165  canthp1lem2  10166  gchdju1  10169  gchinf  10170  pwfseqlem5  10176  pwdjundom  10180  gchdjuidm  10181  gchxpidm  10182  gchhar  10192  inttsk  10287  tskcard  10294  r1tskina  10295  tskuni  10296  hashkf  13797  fz1isolem  13926  isercolllem2  15128  summolem2  15179  zsum  15181  prodmolem2  15394  zprod  15396  4sqlem11  16404  mreexexd  17035  psgnunilem1  18752  simpgnsgd  19354  frlmisfrlm  20677  frlmiscvec  20678  ovoliunlem1  24267  rabfodom  30438  unidifsnel  30470  unidifsnne  30471  fnpreimac  30596  padct  30642  lindsdom  35427  matunitlindflem2  35430  heicant  35468  mblfinlem1  35470  eldioph2lem1  40195  isnumbasgrplem3  40543  fiuneneq  40635  harval3  40738  enrelmap  41192  enmappw  41194