Theorem ensymd 8937

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

Syntax hints:   → wi 4   class class class wbr 5095   ≈ cen 8876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-er 8632  df-en 8880

This theorem is referenced by:  f1imaeng  8946  f1imaen2g  8947  xpdom3  8999  omxpen  9003  mapdom2  9072  mapdom3  9073  limensuci  9077  unxpdom2  9159  sucxpdom  9160  fiintOLD  9236  marypha1lem  9342  infdifsn  9572  cnfcom2lem  9616  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  10493  canthp1lem1  10565  canthp1lem2  10566  gchdju1  10569  gchinf  10570  pwfseqlem5  10576  pwdjundom  10580  gchdjuidm  10581  gchxpidm  10582  gchhar  10592  inttsk  10687  tskcard  10694  r1tskina  10695  tskuni  10696  hashkf  14257  fz1isolem  14386  isercolllem2  15591  summolem2  15641  zsum  15643  prodmolem2  15860  zprod  15862  4sqlem11  16885  mreexexd  17572  psgnunilem1  19390  simpgnsgd  19999  frlmisfrlm  21773  frlmiscvec  21774  ovoliunlem1  25419  rabfodom  32467  unidifsnel  32497  unidifsnne  32498  fnpreimac  32628  padct  32676  hashpss  32767  lindsdom  37593  matunitlindflem2  37596  heicant  37634  mblfinlem1  37636  sticksstones18  42137  sticksstones19  42138  eldioph2lem1  42733  isnumbasgrplem3  43078  fiuneneq  43165  harval3  43511  enrelmap  43970  enmappw  43972