Theorem ensymd 9033

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

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

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 7752

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 3900  df-un 3902  df-in 3904  df-ss 3915  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 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-er 8718  df-en 8975

This theorem is used by:  f1imaeng  9042  f1imaen2g  9043  xpdom3  9095  omxpen  9099  mapdom2  9168  mapdom3  9169  limensuci  9173  unxpdom2  9252  sucxpdom  9253  marypha1lem  9426  infdifsn  9659  cnfcom2lem  9703  karden  9960  cardidm  10041  cardnueq0  10046  carden2a  10048  card1  10050  cardsdomel  10056  isinffi  10074  en2eqpr  10087  infxpenlem  10093  infxpidm2  10097  alephnbtwn2  10152  alephsucdom  10159  mappwen  10192  finnisoeu  10193  djuen  10249  dju1en  10251  djuassen  10258  xpdjuen  10259  infdju1  10269  pwdju1  10270  onadju  10273  cardadju  10274  djunum  10275  nnadju  10277  ficardadju  10279  ficardun  10280  pwsdompw  10282  infdif2  10288  infxp  10293  ackbij1lem5  10302  cfss  10344  ominf4  10391  isfin4p1  10394  fin23lem27  10407  alephsuc3  10666  canthp1lem1  10738  canthp1lem2  10739  gchdju1  10742  gchinf  10743  pwfseqlem5  10749  pwdjundom  10753  gchdjuidm  10754  gchxpidm  10755  gchhar  10765  inttsk  10860  tskcard  10867  r1tskina  10868  tskuni  10869  hashkf  14477  hashpss  14555  fz1isolem  14607  isercolllem2  15834  summolem2  15883  zsum  15885  prodmolem2  16103  zprod  16105  4sqlem11  17134  mreexexd  17823  psgnunilem1  19708  simpgnsgd  20317  frlmisfrlm  22155  frlmiscvec  22156  lindsdom  22157  matunitlindflem2  22996  ovoliunlem1  25824  rabfodom  33102  unidifsnel  33132  unidifsnne  33133  fnpreimac  33265  hashimaf1  33403  soinfdom  35718  1enumen  35724  heicant  38575  mblfinlem1  38577  sticksstones18  43216  sticksstones19  43217  eldioph2lem1  43772  isnumbasgrplem3  44108  fiuneneq  44195  harval3  44540  enrelmap  44998  enmappw  45000