Theorem ensymd 9036

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

This proof depends on syntax axioms:   → wi 4   class class class wbr 5102   ≈ cen 8974

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pow 5326  ax-pr 5390  ax-un 7752

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-er 8721  df-en 8978

This theorem is used by:  f1imaeng  9045  f1imaen2g  9046  xpdom3  9098  omxpen  9102  mapdom2  9171  mapdom3  9172  limensuci  9176  unxpdom2  9255  sucxpdom  9256  marypha1lem  9429  infdifsn  9662  cnfcom2lem  9706  karden  9963  cardidm  10044  cardnueq0  10049  carden2a  10051  card1  10053  cardsdomel  10059  isinffi  10077  en2eqpr  10090  infxpenlem  10096  infxpidm2  10100  alephnbtwn2  10155  alephsucdom  10162  mappwen  10195  finnisoeu  10196  djuen  10252  dju1en  10254  djuassen  10261  xpdjuen  10262  infdju1  10272  pwdju1  10273  onadju  10276  cardadju  10277  djunum  10278  nnadju  10280  ficardadju  10282  ficardun  10283  pwsdompw  10285  infdif2  10291  infxp  10296  ackbij1lem5  10305  cfss  10347  ominf4  10394  isfin4p1  10397  fin23lem27  10410  alephsuc3  10669  canthp1lem1  10741  canthp1lem2  10742  gchdju1  10745  gchinf  10746  pwfseqlem5  10752  pwdjundom  10756  gchdjuidm  10757  gchxpidm  10758  gchhar  10768  inttsk  10863  tskcard  10870  r1tskina  10871  tskuni  10872  hashkf  14480  hashpss  14558  fz1isolem  14610  isercolllem2  15839  summolem2  15888  zsum  15890  prodmolem2  16108  zprod  16110  4sqlem11  17139  mreexexd  17828  psgnunilem1  19713  simpgnsgd  20322  frlmisfrlm  22160  frlmiscvec  22161  lindsdom  22162  matunitlindflem2  23001  ovoliunlem1  25829  rabfodom  33149  unidifsnel  33179  unidifsnne  33180  fnpreimac  33312  hashimaf1  33449  soinfdom  35769  1enumen  35776  heicant  38667  mblfinlem1  38669  sticksstones18  43308  sticksstones19  43309  eldioph2lem1  43865  isnumbasgrplem3  44201  fiuneneq  44288  harval3  44633  enrelmap  45091  enmappw  45093