Theorem ensymd 8982

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

Syntax hints:   → wi 4   class class class wbr 5099   ≈ cen 8920

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-pow 5321  ax-pr 5389  ax-un 7714

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-id 5540  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658  df-fun 6519  df-fn 6520  df-f 6521  df-f1 6522  df-fo 6523  df-f1o 6524  df-er 8673  df-en 8924

This theorem is referenced by:  f1imaeng  8991  f1imaen2g  8992  xpdom3  9043  omxpen  9047  mapdom2  9116  mapdom3  9117  limensuci  9121  unxpdom2  9200  sucxpdom  9201  marypha1lem  9376  infdifsn  9609  cnfcom2lem  9653  cardidm  9914  cardnueq0  9919  carden2a  9921  card1  9923  cardsdomel  9929  isinffi  9947  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  10219  ominf4  10266  isfin4p1  10269  fin23lem27  10282  alephsuc3  10535  canthp1lem1  10607  canthp1lem2  10608  gchdju1  10611  gchinf  10612  pwfseqlem5  10618  pwdjundom  10622  gchdjuidm  10623  gchxpidm  10624  gchhar  10634  inttsk  10729  tskcard  10736  r1tskina  10737  tskuni  10738  hashkf  14342  fz1isolem  14471  isercolllem2  15676  summolem2  15726  zsum  15728  prodmolem2  15948  zprod  15950  4sqlem11  16974  mreexexd  17663  psgnunilem1  19516  simpgnsgd  20125  frlmisfrlm  21880  frlmiscvec  21881  ovoliunlem1  25544  rabfodom  32653  unidifsnel  32683  unidifsnne  32684  fnpreimac  32822  hashpss  32961  hashimaf1  32963  lindsdom  38077  matunitlindflem2  38080  heicant  38118  mblfinlem1  38120  sticksstones18  42745  sticksstones19  42746  eldioph2lem1  43305  isnumbasgrplem3  43646  fiuneneq  43733  harval3  44078  enrelmap  44537  enmappw  44539