Theorem ensymd 8945

Description: Symmetry of equinumerosity. Deduction form of ensym 8943. (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 8943	. 2 ⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐵 ≈ 𝐴)

Syntax hints:   → wi 4   class class class wbr 5086   ≈ cen 8883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-pow 5302  ax-pr 5370  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-er 8636  df-en 8887

This theorem is referenced by:  f1imaeng  8954  f1imaen2g  8955  xpdom3  9006  omxpen  9010  mapdom2  9079  mapdom3  9080  limensuci  9084  unxpdom2  9163  sucxpdom  9164  marypha1lem  9339  infdifsn  9569  cnfcom2lem  9613  cardidm  9874  cardnueq0  9879  carden2a  9881  card1  9883  cardsdomel  9889  isinffi  9907  en2eqpr  9920  infxpenlem  9926  infxpidm2  9930  alephnbtwn2  9985  alephsucdom  9992  mappwen  10025  finnisoeu  10026  djuen  10083  dju1en  10085  djuassen  10092  xpdjuen  10093  infdju1  10103  pwdju1  10104  onadju  10107  cardadju  10108  djunum  10109  nnadju  10111  ficardadju  10113  ficardun  10114  pwsdompw  10116  infdif2  10122  infxp  10127  ackbij1lem5  10136  cfss  10178  ominf4  10225  isfin4p1  10228  fin23lem27  10241  alephsuc3  10494  canthp1lem1  10566  canthp1lem2  10567  gchdju1  10570  gchinf  10571  pwfseqlem5  10577  pwdjundom  10581  gchdjuidm  10582  gchxpidm  10583  gchhar  10593  inttsk  10688  tskcard  10695  r1tskina  10696  tskuni  10697  hashkf  14285  fz1isolem  14414  isercolllem2  15619  summolem2  15669  zsum  15671  prodmolem2  15891  zprod  15893  4sqlem11  16917  mreexexd  17605  psgnunilem1  19459  simpgnsgd  20068  frlmisfrlm  21838  frlmiscvec  21839  ovoliunlem1  25479  rabfodom  32590  unidifsnel  32620  unidifsnne  32621  fnpreimac  32758  hashpss  32897  hashimaf1  32899  lindsdom  37949  matunitlindflem2  37952  heicant  37990  mblfinlem1  37992  sticksstones18  42617  sticksstones19  42618  eldioph2lem1  43206  isnumbasgrplem3  43551  fiuneneq  43638  harval3  43983  enrelmap  44442  enmappw  44444