Theorem ensymd 8723

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

Syntax hints:   → wi 4   class class class wbr 5070   ≈ cen 8665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-sep 5216  ax-nul 5223  ax-pow 5282  ax-pr 5346  ax-un 7563

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3425  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4255  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-id 5479  df-xp 5585  df-rel 5586  df-cnv 5587  df-co 5588  df-dm 5589  df-rn 5590  df-res 5591  df-ima 5592  df-fun 6417  df-fn 6418  df-f 6419  df-f1 6420  df-fo 6421  df-f1o 6422  df-er 8433  df-en 8669

This theorem is referenced by:  f1imaeng  8732  f1imaen2g  8733  en2snOLDOLD  8764  xpdom3  8787  omxpen  8791  mapdom2  8861  mapdom3  8862  limensuci  8866  phplem4  8872  php  8874  unxpdom2  8934  sucxpdom  8935  fiint  8996  marypha1lem  9097  infdifsn  9320  cnfcom2lem  9364  cardidm  9623  cardnueq0  9628  carden2a  9630  card1  9632  cardsdomel  9638  isinffi  9656  en2eqpr  9669  infxpenlem  9675  infxpidm2  9679  alephnbtwn2  9734  alephsucdom  9741  mappwen  9774  finnisoeu  9775  djuen  9831  dju1en  9833  djuassen  9840  xpdjuen  9841  infdju1  9851  pwdju1  9852  onadju  9855  cardadju  9856  djunum  9857  nnadju  9859  ficardadju  9861  ficardun  9862  ficardunOLD  9863  pwsdompw  9866  infdif2  9872  infxp  9877  ackbij1lem5  9886  cfss  9927  ominf4  9974  isfin4p1  9977  fin23lem27  9990  alephsuc3  10242  canthp1lem1  10314  canthp1lem2  10315  gchdju1  10318  gchinf  10319  pwfseqlem5  10325  pwdjundom  10329  gchdjuidm  10330  gchxpidm  10331  gchhar  10341  inttsk  10436  tskcard  10443  r1tskina  10444  tskuni  10445  hashkf  13949  fz1isolem  14078  isercolllem2  15280  summolem2  15331  zsum  15333  prodmolem2  15548  zprod  15550  4sqlem11  16559  mreexexd  17249  psgnunilem1  18991  simpgnsgd  19593  frlmisfrlm  20940  frlmiscvec  20941  ovoliunlem1  24546  rabfodom  30727  unidifsnel  30759  unidifsnne  30760  fnpreimac  30885  padct  30931  lindsdom  35677  matunitlindflem2  35680  heicant  35718  mblfinlem1  35720  sticksstones18  40020  sticksstones19  40021  eldioph2lem1  40470  isnumbasgrplem3  40818  fiuneneq  40910  harval3  41013  enrelmap  41467  enmappw  41469