Theorem ensymd 9045

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

Syntax hints:   → wi 4   class class class wbr 5143   ≈ cen 8982

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-er 8745  df-en 8986

This theorem is referenced by:  f1imaeng  9054  f1imaen2g  9055  xpdom3  9110  omxpen  9114  mapdom2  9188  mapdom3  9189  limensuci  9193  phplem4OLD  9257  phpOLD  9259  unxpdom2  9290  sucxpdom  9291  fiintOLD  9367  marypha1lem  9473  infdifsn  9697  cnfcom2lem  9741  cardidm  9999  cardnueq0  10004  carden2a  10006  card1  10008  cardsdomel  10014  isinffi  10032  en2eqpr  10047  infxpenlem  10053  infxpidm2  10057  alephnbtwn2  10112  alephsucdom  10119  mappwen  10152  finnisoeu  10153  djuen  10210  dju1en  10212  djuassen  10219  xpdjuen  10220  infdju1  10230  pwdju1  10231  onadju  10234  cardadju  10235  djunum  10236  nnadju  10238  ficardadju  10240  ficardun  10241  pwsdompw  10243  infdif2  10249  infxp  10254  ackbij1lem5  10263  cfss  10305  ominf4  10352  isfin4p1  10355  fin23lem27  10368  alephsuc3  10620  canthp1lem1  10692  canthp1lem2  10693  gchdju1  10696  gchinf  10697  pwfseqlem5  10703  pwdjundom  10707  gchdjuidm  10708  gchxpidm  10709  gchhar  10719  inttsk  10814  tskcard  10821  r1tskina  10822  tskuni  10823  hashkf  14371  fz1isolem  14500  isercolllem2  15702  summolem2  15752  zsum  15754  prodmolem2  15971  zprod  15973  4sqlem11  16993  mreexexd  17691  psgnunilem1  19511  simpgnsgd  20120  frlmisfrlm  21868  frlmiscvec  21869  ovoliunlem1  25537  rabfodom  32524  unidifsnel  32553  unidifsnne  32554  fnpreimac  32681  padct  32731  hashpss  32813  lindsdom  37621  matunitlindflem2  37624  heicant  37662  mblfinlem1  37664  sticksstones18  42165  sticksstones19  42166  eldioph2lem1  42771  isnumbasgrplem3  43117  fiuneneq  43204  harval3  43551  enrelmap  44010  enmappw  44012