Theorem ensymd 8956

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

Syntax hints:   → wi 4   class class class wbr 5100   ≈ cen 8894

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 5245  ax-pow 5314  ax-pr 5381  ax-un 7692

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-id 5529  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-er 8647  df-en 8898

This theorem is referenced by:  f1imaeng  8965  f1imaen2g  8966  xpdom3  9017  omxpen  9021  mapdom2  9090  mapdom3  9091  limensuci  9095  unxpdom2  9174  sucxpdom  9175  marypha1lem  9350  infdifsn  9580  cnfcom2lem  9624  cardidm  9885  cardnueq0  9890  carden2a  9892  card1  9894  cardsdomel  9900  isinffi  9918  en2eqpr  9931  infxpenlem  9937  infxpidm2  9941  alephnbtwn2  9996  alephsucdom  10003  mappwen  10036  finnisoeu  10037  djuen  10094  dju1en  10096  djuassen  10103  xpdjuen  10104  infdju1  10114  pwdju1  10115  onadju  10118  cardadju  10119  djunum  10120  nnadju  10122  ficardadju  10124  ficardun  10125  pwsdompw  10127  infdif2  10133  infxp  10138  ackbij1lem5  10147  cfss  10189  ominf4  10236  isfin4p1  10239  fin23lem27  10252  alephsuc3  10505  canthp1lem1  10577  canthp1lem2  10578  gchdju1  10581  gchinf  10582  pwfseqlem5  10588  pwdjundom  10592  gchdjuidm  10593  gchxpidm  10594  gchhar  10604  inttsk  10699  tskcard  10706  r1tskina  10707  tskuni  10708  hashkf  14269  fz1isolem  14398  isercolllem2  15603  summolem2  15653  zsum  15655  prodmolem2  15872  zprod  15874  4sqlem11  16897  mreexexd  17585  psgnunilem1  19439  simpgnsgd  20048  frlmisfrlm  21820  frlmiscvec  21821  ovoliunlem1  25476  rabfodom  32598  unidifsnel  32628  unidifsnne  32629  fnpreimac  32766  hashpss  32906  hashimaf1  32908  lindsdom  37894  matunitlindflem2  37897  heicant  37935  mblfinlem1  37937  sticksstones18  42563  sticksstones19  42564  eldioph2lem1  43146  isnumbasgrplem3  43491  fiuneneq  43578  harval3  43923  enrelmap  44382  enmappw  44384