Theorem ensymd 8543

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

Syntax hints:   → wi 4   class class class wbr 5030   ≈ cen 8489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-er 8272  df-en 8493

This theorem is referenced by:  f1imaeng  8552  f1imaen2g  8553  en2sn  8576  xpdom3  8598  omxpen  8602  mapdom2  8672  mapdom3  8673  limensuci  8677  phplem4  8683  php  8685  unxpdom2  8710  sucxpdom  8711  fiint  8779  marypha1lem  8881  infdifsn  9104  cnfcom2lem  9148  cardidm  9372  cardnueq0  9377  carden2a  9379  card1  9381  cardsdomel  9387  isinffi  9405  en2eqpr  9418  infxpenlem  9424  infxpidm2  9428  alephnbtwn2  9483  alephsucdom  9490  mappwen  9523  finnisoeu  9524  djuen  9580  dju1en  9582  djuassen  9589  xpdjuen  9590  infdju1  9600  pwdju1  9601  onadju  9604  cardadju  9605  djunum  9606  nnadju  9608  ficardadju  9610  ficardun  9611  ficardunOLD  9612  pwsdompw  9615  infdif2  9621  infxp  9626  ackbij1lem5  9635  cfss  9676  ominf4  9723  isfin4p1  9726  fin23lem27  9739  alephsuc3  9991  canthp1lem1  10063  canthp1lem2  10064  gchdju1  10067  gchinf  10068  pwfseqlem5  10074  pwdjundom  10078  gchdjuidm  10079  gchxpidm  10080  gchhar  10090  inttsk  10185  tskcard  10192  r1tskina  10193  tskuni  10194  hashkf  13688  fz1isolem  13815  isercolllem2  15014  summolem2  15065  zsum  15067  prodmolem2  15281  zprod  15283  4sqlem11  16281  mreexexd  16911  psgnunilem1  18613  simpgnsgd  19215  frlmisfrlm  20537  frlmiscvec  20538  ovoliunlem1  24106  rabfodom  30274  unidifsnel  30307  unidifsnne  30308  fnpreimac  30434  padct  30481  lindsdom  35051  matunitlindflem2  35054  heicant  35092  mblfinlem1  35094  eldioph2lem1  39701  isnumbasgrplem3  40049  fiuneneq  40141  harval3  40244  enrelmap  40698  enmappw  40700