Theorem ensymd 9016

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

This proof depends on syntax axioms:   → wi 4   class class class wbr 5103   ≈ cen 8954

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-pow 5327  ax-pr 5391  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-er 8701  df-en 8958

This theorem is used by:  f1imaeng  9025  f1imaen2g  9026  xpdom3  9078  omxpen  9082  mapdom2  9151  mapdom3  9152  limensuci  9156  unxpdom2  9235  sucxpdom  9236  marypha1lem  9409  infdifsn  9642  cnfcom2lem  9686  karden  9940  cardidm  10021  cardnueq0  10026  carden2a  10028  card1  10030  cardsdomel  10036  isinffi  10054  en2eqpr  10067  infxpenlem  10073  infxpidm2  10077  alephnbtwn2  10132  alephsucdom  10139  mappwen  10172  finnisoeu  10173  djuen  10229  dju1en  10231  djuassen  10238  xpdjuen  10239  infdju1  10249  pwdju1  10250  onadju  10253  cardadju  10254  djunum  10255  nnadju  10257  ficardadju  10259  ficardun  10260  pwsdompw  10262  infdif2  10268  infxp  10273  ackbij1lem5  10282  cfss  10324  ominf4  10371  isfin4p1  10374  fin23lem27  10387  alephsuc3  10646  canthp1lem1  10718  canthp1lem2  10719  gchdju1  10722  gchinf  10723  pwfseqlem5  10729  pwdjundom  10733  gchdjuidm  10734  gchxpidm  10735  gchhar  10745  inttsk  10840  tskcard  10847  r1tskina  10848  tskuni  10849  hashkf  14456  hashpss  14534  fz1isolem  14586  isercolllem2  15813  summolem2  15862  zsum  15864  prodmolem2  16082  zprod  16084  4sqlem11  17113  mreexexd  17802  psgnunilem1  19687  simpgnsgd  20296  frlmisfrlm  22134  frlmiscvec  22135  lindsdom  22136  matunitlindflem2  22975  ovoliunlem1  25803  rabfodom  33083  unidifsnel  33113  unidifsnne  33114  fnpreimac  33246  hashimaf1  33384  1enumen  35702  heicant  38541  mblfinlem1  38543  sticksstones18  43182  sticksstones19  43183  eldioph2lem1  43724  isnumbasgrplem3  44065  fiuneneq  44152  harval3  44497  enrelmap  44956  enmappw  44958