Theorem ensymd 8158

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

Syntax hints:   → wi 4   class class class wbr 4786   ≈ cen 8104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7094

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-fun 6031  df-fn 6032  df-f 6033  df-f1 6034  df-fo 6035  df-f1o 6036  df-er 7894  df-en 8108

This theorem is referenced by:  f1imaeng  8167  f1imaen2g  8168  en2sn  8191  xpdom3  8212  omxpen  8216  mapdom2  8285  mapdom3  8286  limensuci  8290  phplem4  8296  php  8298  unxpdom2  8322  sucxpdom  8323  fiint  8391  marypha1lem  8493  infdifsn  8716  cnfcom2lem  8760  cardidm  8983  cardnueq0  8988  carden2a  8990  card1  8992  cardsdomel  8998  isinffi  9016  en2eqpr  9028  infxpenlem  9034  infxpidm2  9038  alephnbtwn2  9093  alephsucdom  9100  mappwen  9133  finnisoeu  9134  cdaen  9195  cda1en  9197  cdaassen  9204  xpcdaen  9205  infcda1  9215  pwcda1  9216  onacda  9219  cardacda  9220  cdanum  9221  ficardun  9224  pwsdompw  9226  infdif2  9232  infxp  9237  ackbij1lem5  9246  cfss  9287  ominf4  9334  isfin4-3  9337  fin23lem27  9350  alephsuc3  9602  canthp1lem1  9674  gchcda1  9678  gchinf  9679  pwfseqlem5  9685  pwcdandom  9689  gchcdaidm  9690  gchxpidm  9691  gchhar  9701  inttsk  9796  tskcard  9803  r1tskina  9804  tskuni  9805  hashkf  13316  fz1isolem  13440  isercolllem2  14597  summolem2a  14647  summolem2  14648  zsum  14650  prodmolem2a  14864  prodmolem2  14865  zprod  14867  4sqlem11  15859  mreexexd  16509  orbsta2  17947  psgnunilem1  18113  frlmisfrlm  20397  frlmiscvec  20398  ovoliunlem1  23483  rabfodom  29675  padct  29830  lindsdom  33729  matunitlindflem2  33732  heicant  33770  mblfinlem1  33772  eldioph2lem1  37842  isnumbasgrplem3  38194  fiuneneq  38294  enrelmap  38810  enmappw  38812