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

Theorem exbii 1572
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 1571 . 2  |-  ( A. x ( ph  <->  ps )  ->  ( E. x ph  <->  E. x ps ) )
2 exbii.1 . 2  |-  ( ph  <->  ps )
31, 2mpg 1538 1  |-  ( E. x ph  <->  E. x ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 176   E.wex 1531
This theorem is referenced by:  2exbii  1573  3exbii  1574  exanali  1575  exancom  1576  19.43  1595  exiftru  1647  excom13  1829  exrot4  1831  eeor  1838  19.12vv  1851  19.41vv  1855  19.41vvv  1856  19.41vvvv  1857  exdistr  1859  19.42vvv  1861  exdistr2  1862  3exdistr  1863  4exdistr  1864  eean  1865  eeeanv  1867  ee4anv  1868  equsex  1915  2sb5  2064  2sb5rf  2069  sbel2x  2077  exsbOLD  2083  2exsb  2084  sb8eu  2174  eu1  2177  eu2  2181  sbmo  2186  moanim  2212  2moswap  2231  2eu1  2236  exists1  2245  clelab  2416  clabel  2417  sbabel  2458  rexbii2  2585  r2exf  2592  r19.41  2705  isset  2805  rexv  2815  ceqsex2  2837  ceqsex3v  2839  gencbvex  2843  vtocl2  2852  vtocl3  2853  spc3gv  2886  ceqsrexv  2914  rexab  2941  rexrab2  2946  euxfr  2964  euind  2965  reu6  2967  reu3  2968  2reuswap  2980  reuind  2981  2reu5lem3  2985  2reu5  2986  sbccomlem  3074  rmo2  3089  rexun  3368  reupick3  3466  abn0  3486  pssnel  3532  rexsns  3684  snprc  3708  euabsn2  3711  reusn  3713  eusn  3716  elunirab  3856  unipr  3857  uniun  3862  uniin  3863  uni0b  3868  uniintsn  3915  iuncom4  3928  dfiun2g  3951  iunn0  3978  iunxiun  4000  disjor  4023  cbvopab2  4106  cbvopab2v  4109  unopab  4111  axrep1  4148  axrep4  4151  axrep5  4152  zfrep4  4155  axsep  4156  zfnuleu  4162  axnulALT  4163  0ex  4166  vprc  4168  inex1  4171  inuni  4189  axpweq  4203  zfpow  4205  axpow2  4206  axpow3  4207  pwex  4209  zfpair  4228  zfpair2  4231  eqvinop  4267  copsexg  4268  opabn0  4311  iunopab  4312  dfid3  4326  zfun  4529  uniex2  4531  uniuni  4543  reusv5OLD  4560  elxp2  4723  opeliunxp  4756  xpiundi  4759  xpiundir  4760  elvvv  4765  eliunxp  4839  relop  4850  opelco2g  4867  cnvco  4881  cnvuni  4882  dfdm3  4883  dfrn2  4884  dfrn3  4885  elrng  4887  dfdm4  4888  eldm2g  4891  dmun  4901  dmin  4902  dmiun  4903  dmuni  4904  dmopab  4905  dmi  4909  elrn  4935  rnopab  4940  dmcosseq  4962  dmres  4992  elres  5006  elsnres  5007  dfima2  5030  elima3  5035  imadmrn  5040  imai  5043  args  5057  rniun  5107  ssrnres  5132  dmsnn0  5154  dmsnopg  5160  elxp4  5176  elxp5  5177  cnvresima  5178  mptpreima  5182  dfco2  5188  coundi  5190  coundir  5191  resco  5193  imaco  5194  rnco  5195  coiun  5198  coi1  5204  coass  5207  dffun2  5281  dffun5  5284  imadif  5343  funimaexg  5345  fun11iun  5509  f11o  5522  brprcneu  5534  dffv2  5608  fndmin  5648  fvresex  5778  abrexco  5782  opabex3  5785  imaiun  5787  abexssex  5797  abexex  5798  isomin  5850  dfoprab2  5911  cbvoprab2  5935  oprabrexex2  5979  releldm2  6186  dfopab2  6190  dfoprab3s  6191  exopxfr  6199  fsplit  6239  frxp  6241  brtpos2  6256  oarec  6576  oeeu  6617  domen  6891  mapsnen  6954  xpsnen  6962  xpcomco  6968  xpassen  6972  inf2  7340  zfinf  7356  axinf2  7357  zfinf2  7359  rankuni  7551  scott0  7572  cp  7577  ween  7678  aceq1  7760  aceq0  7761  aceq2  7762  dfac5lem1  7766  dfac5lem2  7767  dfac5lem3  7768  kmlem3  7794  kmlem14  7805  kmlem15  7806  kmlem16  7807  cflem  7888  cf0  7893  cfval2  7902  cfss  7907  cfslb  7908  fin23lem32  7986  axdc2lem  8090  zfac  8102  ac9  8126  ac9s  8136  axpowndlem3  8237  zfcndrep  8252  zfcndun  8253  zfcndpow  8254  zfcndinf  8256  zfcndac  8257  axgroth5  8462  axgroth2  8463  grothpw  8464  axgroth6  8466  axgroth3  8469  axgroth4  8470  grothprim  8472  grothtsk  8473  genpass  8649  ltexprlem1  8676  ltexprlem4  8679  supmul1  9735  supmullem2  9737  2rexuz  10287  nnwos  10302  hashfun  11405  maxprmfct  12808  4sqlem12  13019  vdwmc  13041  imasleval  13459  isacs2  13571  gsumval3eu  15206  lidlnz  15996  isbasis2g  16702  tgval2  16710  ntreq0  16830  lmff  17045  cmpfi  17151  is1stc2  17184  1stcelcls  17203  isfbas2  17546  elfg  17582  alexsubALTlem3  17759  metrest  18086  cmetss  18756  dchrvmasumlema  20665  isgrpo  20879  ismgm  21003  2reuswap2  23153  rexunirn  23156  nmo  23160  disjorf  23371  axextprim  24062  axrepprim  24063  axunprim  24064  axpowprim  24065  axregprim  24066  axinfprim  24067  axacprim  24068  cbvcprod  24137  dftr6  24177  coep  24178  coepr  24179  dffr5  24180  dfpo2  24182  cnvco1  24187  cnvco2  24188  eldm3  24189  fundmpss  24192  dfdm5  24202  dfrn5  24203  domep  24219  axextdfeq  24224  19.12b  24228  axextndbi  24231  wfrlem11  24336  tfrALTlem  24346  frrlem5c  24357  nofulllem5  24430  brtxp  24490  brpprod  24495  brsset  24499  dfon3  24502  brtxpsd  24504  elfix  24513  dffix2  24515  dffun10  24523  elfuns  24524  elsingles  24527  snelsingles  24531  dfiota3  24532  brimg  24546  brapply  24547  brcup  24548  brcap  24549  brsuccf  24550  funpartlem  24551  brrestrict  24558  dfrdg4  24559  tfrqfree  24560  supaddc  24994  supadd  24995  itg2addnc  25004  eeeeanv  25046  fates  25057  eqvinopb  25067  islatalg  25285  dfdir2  25393  cbvprodi  25414  apnei  25622  isalg  25823  algi  25829  cnvresimaOLD  26328  neifg  26422  prtlem16  26839  prter2  26851  diophrex  26957  19.36vv  27683  19.37vv  27685  pm11.58  27691  pm11.6  27693  pm13.192  27712  2sbc5g  27718  iotasbc2  27722  rfcnnnub  27809  stoweidlem34  27885  stoweidlem35  27886  stoweidlem60  27911  rmoanim  28059  2rmoswap  28064  opabex3d  28189  3v3e3cycl2  28409  3v3e3cycl  28410  onfrALTlem5  28605  onfrALTlem1  28611  a9e2nd  28622  2sb5nd  28624  en3lplem2VD  28935  relopabVD  28992  a9e2ndVD  28999  2sb5ndVD  29001  a9e2ndALT  29022  2sb5ndALT  29024  bnj89  29062  bnj133  29068  bnj1019  29126  bnj1101  29131  bnj1109  29133  bnj1143  29137  bnj1198  29143  bnj1304  29167  bnj605  29254  bnj607  29263  bnj600  29266  bnj865  29270  bnj916  29280  bnj983  29298  bnj985  29300  bnj996  29302  bnj1033  29314  bnj1083  29323  bnj1090  29324  bnj1093  29325  bnj1110  29327  bnj1128  29335  bnj1145  29338  bnj1171  29345  bnj1172  29346  bnj1174  29348  bnj1176  29350  bnj1186  29352  bnj1189  29354  bnj1253  29362  bnj1279  29363  bnj1371  29374  bnj1374  29376  bnj1312  29403  equsexNEW7  29466  exsbOLDNEW7  29571  2sb5NEW7  29580  sbel2xNEW7  29585  excom13OLD7  29649  exrot4OLD7  29651  eeorOLD7  29653  19.12vvOLD7  29655  eeanOLD7  29656  eeeanvOLD7  29658  ee4anvOLD7  29659  2sb5rfOLD7  29717  2exsbOLD7  29723  equsexv-x12  29735  equvinv  29736  islshpat  29829  islpln5  30346  islvol5  30390  pmapglb  30581  polval2N  30717  cdlemftr3  31376  dibelval3  31959  dicelval3  31992  dihglb2  32154
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547
This theorem depends on definitions:  df-bi 177  df-ex 1532
  Copyright terms: Public domain W3C validator