Theorem ensymd 8791

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

Syntax hints:   → wi 4   class class class wbr 5074   ≈ cen 8730

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-er 8498  df-en 8734

This theorem is referenced by:  f1imaeng  8800  f1imaen2g  8801  en2snOLDOLD  8833  xpdom3  8857  omxpen  8861  mapdom2  8935  mapdom3  8936  limensuci  8940  phplem4OLD  9003  phpOLD  9005  unxpdom2  9031  sucxpdom  9032  fiint  9091  marypha1lem  9192  infdifsn  9415  cnfcom2lem  9459  cardidm  9717  cardnueq0  9722  carden2a  9724  card1  9726  cardsdomel  9732  isinffi  9750  en2eqpr  9763  infxpenlem  9769  infxpidm2  9773  alephnbtwn2  9828  alephsucdom  9835  mappwen  9868  finnisoeu  9869  djuen  9925  dju1en  9927  djuassen  9934  xpdjuen  9935  infdju1  9945  pwdju1  9946  onadju  9949  cardadju  9950  djunum  9951  nnadju  9953  ficardadju  9955  ficardun  9956  ficardunOLD  9957  pwsdompw  9960  infdif2  9966  infxp  9971  ackbij1lem5  9980  cfss  10021  ominf4  10068  isfin4p1  10071  fin23lem27  10084  alephsuc3  10336  canthp1lem1  10408  canthp1lem2  10409  gchdju1  10412  gchinf  10413  pwfseqlem5  10419  pwdjundom  10423  gchdjuidm  10424  gchxpidm  10425  gchhar  10435  inttsk  10530  tskcard  10537  r1tskina  10538  tskuni  10539  hashkf  14046  fz1isolem  14175  isercolllem2  15377  summolem2  15428  zsum  15430  prodmolem2  15645  zprod  15647  4sqlem11  16656  mreexexd  17357  psgnunilem1  19101  simpgnsgd  19703  frlmisfrlm  21055  frlmiscvec  21056  ovoliunlem1  24666  rabfodom  30851  unidifsnel  30883  unidifsnne  30884  fnpreimac  31008  padct  31054  lindsdom  35771  matunitlindflem2  35774  heicant  35812  mblfinlem1  35814  sticksstones18  40120  sticksstones19  40121  eldioph2lem1  40582  isnumbasgrplem3  40930  fiuneneq  41022  harval3  41145  enrelmap  41605  enmappw  41607