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

Theorem exbii 1592
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 1591 . 2  |-  ( A. x ( ph  <->  ps )  ->  ( E. x ph  <->  E. x ps ) )
2 exbii.1 . 2  |-  ( ph  <->  ps )
31, 2mpg 1557 1  |-  ( E. x ph  <->  E. x ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 177   E.wex 1550
This theorem is referenced by:  2exbii  1593  3exbii  1594  exanali  1595  exancom  1596  19.43  1615  exiftruOLD  1670  excom  1756  excom13  1758  exrot4  1760  eeor  1907  19.12vv  1921  19.41vv  1925  19.41vvv  1926  19.41vvvv  1927  exdistr  1929  19.42vvv  1931  exdistr2  1932  3exdistr  1933  4exdistrOLD  1935  eean  1936  eeeanv  1938  eeeanvOLD  1939  ee4anv  1940  equsexOLD  2003  2sb5  2187  2sb5rf  2193  sbel2x  2201  exsbOLD  2207  2exsb  2208  sb8eu  2298  eu1  2301  eu2  2305  sbmo  2310  moanim  2336  2moswap  2355  2eu1  2360  exists1  2369  clelab  2555  clabel  2556  sbabel  2597  rexbii2  2726  r2exf  2733  r19.41  2852  isset  2952  rexv  2962  ceqsex2  2984  ceqsex3v  2986  gencbvex  2990  vtocl2  2999  vtocl3  3000  spc3gv  3033  ceqsrexv  3061  rexab  3089  rexrab2  3094  euxfr  3112  euind  3113  reu6  3115  reu3  3116  2reuswap  3128  reuind  3129  2reu5lem3  3133  2reu5  3134  sbccomlem  3223  rmo2  3238  rexun  3519  reupick3  3618  abn0  3638  pssnel  3685  rexsns  3837  exsnrex  3840  snprc  3863  euabsn2  3867  reusn  3869  eusn  3872  elunirab  4020  unipr  4021  uniun  4026  uniin  4027  uni0b  4032  uniintsn  4079  iuncom4  4092  dfiun2g  4115  iunn0  4143  iunxiun  4165  disjor  4188  cbvopab2  4271  cbvopab2v  4274  unopab  4276  axrep1  4313  axrep4  4316  axrep5  4317  zfrep4  4320  axsep  4321  zfnuleu  4327  axnulALT  4328  0ex  4331  vprc  4333  inex1  4336  inuni  4354  axpweq  4368  zfpow  4370  axpow2  4371  axpow3  4372  pwex  4374  zfpair  4393  zfpair2  4396  eqvinop  4433  copsexg  4434  opabn0  4477  iunopab  4478  dfid3  4491  zfun  4694  uniex2  4696  uniuni  4708  reusv5OLD  4725  elxp2  4888  opeliunxp  4921  xpiundi  4924  xpiundir  4925  elvvv  4929  eliunxp  5004  relop  5015  opelco2g  5032  cnvco  5048  cnvuni  5049  dfdm3  5050  dfrn2  5051  dfrn3  5052  elrng  5054  dfdm4  5055  eldm2g  5058  dmun  5068  dmin  5069  dmiun  5070  dmuni  5071  dmopab  5072  dmi  5076  elrn  5102  rnopab  5107  dmcosseq  5129  dmres  5159  elres  5173  elsnres  5174  dfima2  5197  elima3  5202  imadmrn  5207  imai  5210  args  5224  rniun  5274  ssrnres  5301  dmsnn0  5327  dmsnopg  5333  elxp4  5349  elxp5  5350  cnvresima  5351  mptpreima  5355  dfco2  5361  coundi  5363  coundir  5364  resco  5366  imaco  5367  rnco  5368  coiun  5371  coi1  5377  coass  5380  xpco  5406  dffun2  5456  dffun5  5459  imadif  5520  funimaexg  5522  fun11iun  5687  f11o  5700  brprcneu  5713  dffv2  5788  fndmin  5829  fvresex  5974  abrexco  5978  opabex3d  5981  opabex3  5982  imaiun  5984  abexssex  5994  abexex  5995  isomin  6049  dfoprab2  6113  cbvoprab2  6137  oprabrexex2  6181  releldm2  6389  dfopab2  6393  dfoprab3s  6394  exopxfr  6402  fsplit  6443  frxp  6448  brtpos2  6477  oarec  6797  oeeu  6838  domen  7113  mapsnen  7176  xpsnen  7184  xpcomco  7190  xpassen  7194  inf2  7568  zfinf  7584  axinf2  7585  zfinf2  7587  rankuni  7779  scott0  7800  cp  7805  ween  7906  aceq1  7988  aceq0  7989  aceq2  7990  dfac5lem1  7994  dfac5lem2  7995  dfac5lem3  7996  kmlem3  8022  kmlem14  8033  kmlem15  8034  kmlem16  8035  cflem  8116  cf0  8121  cfval2  8130  cfss  8135  cfslb  8136  fin23lem32  8214  axdc2lem  8318  zfac  8330  ac9  8353  ac9s  8363  axpowndlem3  8464  zfcndrep  8479  zfcndun  8480  zfcndpow  8481  zfcndinf  8483  zfcndac  8484  axgroth5  8689  axgroth2  8690  grothpw  8691  axgroth6  8693  axgroth3  8696  axgroth4  8697  grothprim  8699  grothtsk  8700  genpass  8876  ltexprlem1  8903  ltexprlem4  8906  supmul1  9963  supmullem2  9965  2rexuz  10519  nnwos  10534  hashfun  11690  maxprmfct  13103  4sqlem12  13314  vdwmc  13336  imasleval  13756  isacs2  13868  gsumval3eu  15503  lidlnz  16289  isbasis2g  17003  tgval2  17011  ntreq0  17131  lmff  17355  cmpfi  17461  is1stc2  17495  1stcelcls  17514  isfbas2  17857  elfg  17893  alexsubALTlem3  18070  ustfilxp  18232  metrest  18544  metuel2  18599  restmetu  18607  cmetss  19257  dchrvmasumlema  21184  usgraedg4  21396  3v3e3cycl2  21641  isgrpo  21774  ismgm  21898  nmo  23963  2reuswap2  23965  rexunirn  23968  disjorf  24011  axextprim  25140  axrepprim  25141  axunprim  25142  axpowprim  25143  axregprim  25144  axinfprim  25145  axacprim  25146  cbvprod  25231  iprodmul  25306  dftr6  25363  coep  25364  coepr  25365  dffr5  25366  dfpo2  25368  cnvco1  25373  cnvco2  25374  eldm3  25375  fundmpss  25378  dfdm5  25388  dfrn5  25389  elima4  25392  domep  25408  axextdfeq  25413  19.12b  25417  axextndbi  25420  wfrlem11  25533  tfrALTlem  25542  frrlem5c  25553  nofulllem5  25626  brtxp  25690  brpprod  25695  brsset  25699  dfon3  25702  brtxpsd  25704  elfix  25713  dffix2  25715  sscoid  25723  dffun10  25724  elfuns  25725  elsingles  25728  snelsingles  25732  dfiota3  25733  brimg  25747  brapply  25748  brcup  25749  brcap  25750  brsuccf  25751  funpartlem  25752  brrestrict  25759  dfrdg4  25760  tfrqfree  25761  supaddc  26201  supadd  26202  ismblfin  26210  itg2addnclem3  26221  itg2addnc  26222  neifg  26354  prtlem16  26672  prter2  26684  diophrex  26788  19.36vv  27513  19.37vv  27515  pm11.58  27521  pm11.6  27523  pm13.192  27542  2sbc5g  27548  iotasbc2  27552  rfcnnnub  27638  stoweidlem34  27714  stoweidlem35  27715  stoweidlem60  27740  rmoanim  27888  2rmoswap  27893  cshwssizesame  28215  el2wlkonot  28253  el2spthonot  28254  el2wlkonotot0  28256  frgrawopreglem2  28335  usg2spot2nb  28355  onfrALTlem5  28529  onfrALTlem1  28535  a9e2nd  28546  2sb5nd  28548  en3lplem2VD  28857  relopabVD  28914  a9e2ndVD  28921  2sb5ndVD  28923  a9e2ndALT  28943  2sb5ndALT  28945  bnj89  28987  bnj133  28993  bnj1019  29051  bnj1101  29056  bnj1109  29058  bnj1143  29062  bnj1198  29068  bnj1304  29092  bnj605  29179  bnj607  29188  bnj600  29191  bnj865  29195  bnj916  29205  bnj983  29223  bnj985  29225  bnj996  29227  bnj1033  29239  bnj1083  29248  bnj1090  29249  bnj1093  29250  bnj1110  29252  bnj1128  29260  bnj1145  29263  bnj1171  29270  bnj1172  29271  bnj1174  29273  bnj1176  29275  bnj1186  29277  bnj1189  29279  bnj1253  29287  bnj1279  29288  bnj1371  29299  bnj1374  29301  bnj1312  29328  equsexNEW7  29391  exsbOLDNEW7  29501  2sb5NEW7  29510  sbel2xNEW7  29515  excom13OLD7  29596  exrot4OLD7  29598  eeorOLD7  29600  19.12vvOLD7  29602  eeanOLD7  29603  eeeanvOLD7  29605  ee4anvOLD7  29606  2sb5rfOLD7  29662  2exsbOLD7  29668  islshpat  29716  islpln5  30233  islvol5  30277  pmapglb  30468  polval2N  30604  cdlemftr3  31263  dibelval3  31846  dicelval3  31879  dihglb2  32041
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566
This theorem depends on definitions:  df-bi 178  df-ex 1551
  Copyright terms: Public domain W3C validator