MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ensymd Structured version   Visualization version   GIF version

Theorem ensymd 8123
Description: Symmetry of equinumerosity. Deduction form of ensym 8121. (Contributed by David Moews, 1-May-2017.)
Hypothesis
Ref Expression
ensymd.1 (𝜑𝐴𝐵)
Assertion
Ref Expression
ensymd (𝜑𝐵𝐴)

Proof of Theorem ensymd
StepHypRef Expression
1 ensymd.1 . 2 (𝜑𝐴𝐵)
2 ensym 8121 . 2 (𝐴𝐵𝐵𝐴)
31, 2syl 17 1 (𝜑𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   class class class wbr 4760  cen 8069
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ral 3019  df-rex 3020  df-rab 3023  df-v 3306  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-op 4292  df-uni 4545  df-br 4761  df-opab 4821  df-id 5128  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-fun 6003  df-fn 6004  df-f 6005  df-f1 6006  df-fo 6007  df-f1o 6008  df-er 7862  df-en 8073
This theorem is referenced by:  f1imaeng  8132  f1imaen2g  8133  en2sn  8153  xpdom3  8174  omxpen  8178  mapdom2  8247  mapdom3  8248  limensuci  8252  phplem4  8258  php  8260  unxpdom2  8284  sucxpdom  8285  fiint  8353  marypha1lem  8455  infdifsn  8667  cnfcom2lem  8711  cardidm  8898  cardnueq0  8903  carden2a  8905  card1  8907  cardsdomel  8913  isinffi  8931  en2eqpr  8943  infxpenlem  8949  infxpidm2  8953  alephnbtwn2  9008  alephsucdom  9015  mappwen  9048  finnisoeu  9049  cdaen  9108  cda1en  9110  cdaassen  9117  xpcdaen  9118  infcda1  9128  pwcda1  9129  onacda  9132  cardacda  9133  cdanum  9134  ficardun  9137  pwsdompw  9139  infdif2  9145  infxp  9150  ackbij1lem5  9159  cfss  9200  ominf4  9247  isfin4-3  9250  fin23lem27  9263  alephsuc3  9515  canthp1lem1  9587  gchcda1  9591  gchinf  9592  pwfseqlem5  9598  pwcdandom  9602  gchcdaidm  9603  gchxpidm  9604  gchhar  9614  inttsk  9709  tskcard  9716  r1tskina  9717  tskuni  9718  hashkf  13234  fz1isolem  13358  isercolllem2  14516  summolem2a  14566  summolem2  14567  zsum  14569  prodmolem2a  14784  prodmolem2  14785  zprod  14787  4sqlem11  15782  mreexexd  16431  orbsta2  17868  psgnunilem1  18034  frlmisfrlm  20310  frlmiscvec  20311  ovoliunlem1  23391  rabfodom  29572  padct  29727  lindsdom  33635  matunitlindflem2  33638  heicant  33676  mblfinlem1  33678  eldioph2lem1  37742  isnumbasgrplem3  38094  fiuneneq  38194  enrelmap  38710  enmappw  38712
  Copyright terms: Public domain W3C validator