MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exbii Structured version   Unicode version

Theorem exbii 1593
Description: Inference adding existential quantifier to both sides of an equivalence. (Contributed by NM, 24-May-1994.)
Hypothesis
Ref Expression
exbii.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
exbii  |-  ( E. x ph  <->  E. x ps )

Proof of Theorem exbii
StepHypRef Expression
1 exbi 1592 . 2  |-  ( A. x ( ph  <->  ps )  ->  ( E. x ph  <->  E. x ps ) )
2 exbii.1 . 2  |-  ( ph  <->  ps )
31, 2mpg 1558 1  |-  ( E. x ph  <->  E. x ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 178   E.wex 1551
This theorem is referenced by:  2exbii  1594  3exbii  1595  exanali  1596  exancom  1597  19.43  1616  exiftruOLD  1671  excom  1757  excom13  1759  exrot4  1761  eeor  1908  19.12vv  1922  19.41vv  1926  19.41vvv  1927  19.41vvvv  1928  exdistr  1930  19.42vvv  1932  exdistr2  1933  3exdistr  1934  4exdistrOLD  1936  eean  1937  eeeanv  1939  eeeanvOLD  1940  ee4anv  1941  equsexOLD  2004  2sb5  2190  2sb5rf  2196  sbel2x  2204  exsbOLD  2210  2exsb  2211  sb8eu  2301  eu1  2304  eu2  2308  sbmo  2313  moanim  2339  2moswap  2358  2eu1  2363  exists1  2372  clelab  2558  clabel  2559  sbabel  2600  rexbii2  2736  r2exf  2743  r19.41  2862  isset  2962  rexv  2972  ceqsex2  2994  ceqsex3v  2996  gencbvex  3000  vtocl2  3009  vtocl3  3010  spc3gv  3043  ceqsrexv  3071  rexab  3099  rexrab2  3104  euxfr  3122  euind  3123  reu6  3125  reu3  3126  2reuswap  3138  reuind  3139  2reu5lem3  3143  2reu5  3144  sbccomlem  3233  rmo2  3248  rexun  3529  reupick3  3628  abn0  3648  pssnel  3695  rexsns  3847  exsnrex  3850  snprc  3873  euabsn2  3877  reusn  3879  eusn  3882  elunirab  4030  unipr  4031  uniun  4036  uniin  4037  uni0b  4042  uniintsn  4089  iuncom4  4102  dfiun2g  4125  iunn0  4153  iunxiun  4176  disjor  4199  cbvopab2  4282  cbvopab2v  4285  unopab  4287  axrep1  4324  axrep4  4327  axrep5  4328  zfrep4  4331  axsep  4332  zfnuleu  4338  axnulALT  4339  0ex  4342  vprc  4344  inex1  4347  inuni  4365  axpweq  4379  zfpow  4381  axpow2  4382  axpow3  4383  pwex  4385  zfpair  4404  zfpair2  4407  eqvinop  4444  copsexg  4445  opabn0  4488  iunopab  4489  dfid3  4502  zfun  4705  uniex2  4707  uniuni  4719  reusv5OLD  4736  elxp2  4899  opeliunxp  4932  xpiundi  4935  xpiundir  4936  elvvv  4940  eliunxp  5015  relop  5026  opelco2g  5043  cnvco  5059  cnvuni  5060  dfdm3  5061  dfrn2  5062  dfrn3  5063  elrng  5065  dfdm4  5066  eldm2g  5069  dmun  5079  dmin  5080  dmiun  5081  dmuni  5082  dmopab  5083  dmi  5087  elrn  5113  rnopab  5118  dmcosseq  5140  dmres  5170  elres  5184  elsnres  5185  dfima2  5208  elima3  5213  imadmrn  5218  imai  5221  args  5235  rniun  5285  ssrnres  5312  dmsnn0  5338  dmsnopg  5344  elxp4  5360  elxp5  5361  cnvresima  5362  mptpreima  5366  dfco2  5372  coundi  5374  coundir  5375  resco  5377  imaco  5378  rnco  5379  coiun  5382  coi1  5388  coass  5391  xpco  5417  dffun2  5467  dffun5  5470  imadif  5531  funimaexg  5533  fun11iun  5698  f11o  5711  brprcneu  5724  dffv2  5799  fndmin  5840  fvresex  5985  abrexco  5989  opabex3d  5992  opabex3  5993  imaiun  5995  abexssex  6005  abexex  6006  isomin  6060  dfoprab2  6124  cbvoprab2  6148  oprabrexex2  6192  releldm2  6400  dfopab2  6404  dfoprab3s  6405  exopxfr  6413  fsplit  6454  frxp  6459  brtpos2  6488  oarec  6808  oeeu  6849  domen  7124  mapsnen  7187  xpsnen  7195  xpcomco  7201  xpassen  7205  inf2  7581  zfinf  7597  axinf2  7598  zfinf2  7600  rankuni  7792  scott0  7815  cp  7820  ween  7921  aceq1  8003  aceq0  8004  aceq2  8005  dfac5lem1  8009  dfac5lem2  8010  dfac5lem3  8011  kmlem3  8037  kmlem14  8048  kmlem15  8049  kmlem16  8050  cflem  8131  cf0  8136  cfval2  8145  cfss  8150  cfslb  8151  fin23lem32  8229  axdc2lem  8333  zfac  8345  ac9  8368  ac9s  8378  axpowndlem3  8479  zfcndrep  8494  zfcndun  8495  zfcndpow  8496  zfcndinf  8498  zfcndac  8499  axgroth5  8704  axgroth2  8705  grothpw  8706  axgroth6  8708  axgroth3  8711  axgroth4  8712  grothprim  8714  grothtsk  8715  genpass  8891  ltexprlem1  8918  ltexprlem4  8921  supmul1  9978  supmullem2  9980  2rexuz  10534  nnwos  10549  hashfun  11705  maxprmfct  13118  4sqlem12  13329  vdwmc  13351  imasleval  13771  isacs2  13883  gsumval3eu  15518  lidlnz  16304  isbasis2g  17018  tgval2  17026  ntreq0  17146  lmff  17370  cmpfi  17476  is1stc2  17510  1stcelcls  17529  isfbas2  17872  elfg  17908  alexsubALTlem3  18085  ustfilxp  18247  metrest  18559  metuel2  18614  restmetu  18622  cmetss  19272  dchrvmasumlema  21199  usgraedg4  21411  3v3e3cycl2  21656  isgrpo  21789  ismgm  21913  nmo  23978  2reuswap2  23980  rexunirn  23983  disjorf  24026  axextprim  25155  axrepprim  25156  axunprim  25157  axpowprim  25158  axregprim  25159  axinfprim  25160  axacprim  25161  cbvprod  25246  iprodmul  25321  dftr6  25378  coep  25379  coepr  25380  dffr5  25381  dfpo2  25383  cnvco1  25388  cnvco2  25389  eldm3  25390  fundmpss  25395  dfdm5  25405  dfrn5  25406  elima4  25409  domep  25425  axextdfeq  25430  19.12b  25434  axextndbi  25437  wfrlem11  25553  frrlem5c  25593  nofulllem5  25666  brtxp  25730  brpprod  25735  brsset  25739  dfon3  25742  brtxpsd  25744  elfix  25753  dffix2  25755  sscoid  25763  dffun10  25764  elfuns  25765  elsingles  25768  snelsingles  25772  dfiota3  25773  brimg  25787  brapply  25788  brcup  25789  brcap  25790  brsuccf  25791  funpartlem  25792  brrestrict  25799  dfrdg4  25800  tfrqfree  25801  wl-sbequ8  26241  supaddc  26245  supadd  26246  ismblfin  26259  itg2addnclem3  26272  itg2addnc  26273  neifg  26414  prtlem16  26732  prter2  26744  diophrex  26848  19.36vv  27572  19.37vv  27574  pm11.58  27580  pm11.6  27582  pm13.192  27601  2sbc5g  27607  iotasbc2  27611  rfcnnnub  27697  stoweidlem34  27773  stoweidlem35  27774  stoweidlem60  27799  rmoanim  27947  2rmoswap  27952  cshwssizesame  28322  el2wlkonot  28401  el2spthonot  28402  el2wlkonotot0  28404  frgrawopreglem2  28508  usg2spot2nb  28528  onfrALTlem5  28702  onfrALTlem1  28708  a9e2nd  28719  2sb5nd  28721  en3lplem2VD  29030  relopabVD  29087  a9e2ndVD  29094  2sb5ndVD  29096  a9e2ndALT  29116  2sb5ndALT  29118  bnj89  29160  bnj133  29166  bnj1019  29224  bnj1101  29229  bnj1109  29231  bnj1143  29235  bnj1198  29241  bnj1304  29265  bnj605  29352  bnj607  29361  bnj600  29364  bnj865  29368  bnj916  29378  bnj983  29396  bnj985  29398  bnj996  29400  bnj1033  29412  bnj1083  29421  bnj1090  29422  bnj1093  29423  bnj1110  29425  bnj1128  29433  bnj1145  29436  bnj1171  29443  bnj1172  29444  bnj1174  29446  bnj1176  29448  bnj1186  29450  bnj1189  29452  bnj1253  29460  bnj1279  29461  bnj1371  29472  bnj1374  29474  bnj1312  29501  equsexNEW7  29564  exsbOLDNEW7  29674  2sb5NEW7  29683  sbel2xNEW7  29688  excom13OLD7  29769  exrot4OLD7  29771  eeorOLD7  29773  19.12vvOLD7  29775  eeanOLD7  29776  eeeanvOLD7  29778  ee4anvOLD7  29779  2sb5rfOLD7  29835  2exsbOLD7  29841  islshpat  29889  islpln5  30406  islvol5  30450  pmapglb  30641  polval2N  30777  cdlemftr3  31436  dibelval3  32019  dicelval3  32052  dihglb2  32214
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567
This theorem depends on definitions:  df-bi 179  df-ex 1552
  Copyright terms: Public domain W3C validator