Theorem ensymd 8976

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

Syntax hints:   → wi 4   class class class wbr 5107   ≈ cen 8915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-er 8671  df-en 8919

This theorem is referenced by:  f1imaeng  8985  f1imaen2g  8986  xpdom3  9039  omxpen  9043  mapdom2  9112  mapdom3  9113  limensuci  9117  unxpdom2  9201  sucxpdom  9202  fiintOLD  9278  marypha1lem  9384  infdifsn  9610  cnfcom2lem  9654  cardidm  9912  cardnueq0  9917  carden2a  9919  card1  9921  cardsdomel  9927  isinffi  9945  en2eqpr  9960  infxpenlem  9966  infxpidm2  9970  alephnbtwn2  10025  alephsucdom  10032  mappwen  10065  finnisoeu  10066  djuen  10123  dju1en  10125  djuassen  10132  xpdjuen  10133  infdju1  10143  pwdju1  10144  onadju  10147  cardadju  10148  djunum  10149  nnadju  10151  ficardadju  10153  ficardun  10154  pwsdompw  10156  infdif2  10162  infxp  10167  ackbij1lem5  10176  cfss  10218  ominf4  10265  isfin4p1  10268  fin23lem27  10281  alephsuc3  10533  canthp1lem1  10605  canthp1lem2  10606  gchdju1  10609  gchinf  10610  pwfseqlem5  10616  pwdjundom  10620  gchdjuidm  10621  gchxpidm  10622  gchhar  10632  inttsk  10727  tskcard  10734  r1tskina  10735  tskuni  10736  hashkf  14297  fz1isolem  14426  isercolllem2  15632  summolem2  15682  zsum  15684  prodmolem2  15901  zprod  15903  4sqlem11  16926  mreexexd  17609  psgnunilem1  19423  simpgnsgd  20032  frlmisfrlm  21757  frlmiscvec  21758  ovoliunlem1  25403  rabfodom  32434  unidifsnel  32464  unidifsnne  32465  fnpreimac  32595  padct  32643  hashpss  32734  lindsdom  37608  matunitlindflem2  37611  heicant  37649  mblfinlem1  37651  sticksstones18  42152  sticksstones19  42153  eldioph2lem1  42748  isnumbasgrplem3  43094  fiuneneq  43181  harval3  43527  enrelmap  43986  enmappw  43988