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

Theorem exbii 1589
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 1588 . 2  |-  ( A. x ( ph  <->  ps )  ->  ( E. x ph  <->  E. x ps ) )
2 exbii.1 . 2  |-  ( ph  <->  ps )
31, 2mpg 1554 1  |-  ( E. x ph  <->  E. x ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 177   E.wex 1547
This theorem is referenced by:  2exbii  1590  3exbii  1591  exanali  1592  exancom  1593  19.43  1612  exiftruOLD  1665  excom  1748  excom13  1750  exrot4  1752  eeor  1896  19.12vv  1910  19.41vv  1914  19.41vvv  1915  19.41vvvv  1916  exdistr  1918  19.42vvv  1920  exdistr2  1921  3exdistr  1922  4exdistrOLD  1924  eean  1925  eeeanv  1927  eeeanvOLD  1928  ee4anv  1929  equsexOLD  1950  2sb5  2138  2sb5rf  2144  sbel2x  2152  exsbOLD  2158  2exsb  2159  sb8eu  2249  eu1  2252  eu2  2256  sbmo  2261  moanim  2287  2moswap  2306  2eu1  2311  exists1  2320  clelab  2500  clabel  2501  sbabel  2542  rexbii2  2671  r2exf  2678  r19.41  2796  isset  2896  rexv  2906  ceqsex2  2928  ceqsex3v  2930  gencbvex  2934  vtocl2  2943  vtocl3  2944  spc3gv  2977  ceqsrexv  3005  rexab  3033  rexrab2  3038  euxfr  3056  euind  3057  reu6  3059  reu3  3060  2reuswap  3072  reuind  3073  2reu5lem3  3077  2reu5  3078  sbccomlem  3167  rmo2  3182  rexun  3463  reupick3  3562  abn0  3582  pssnel  3629  rexsns  3781  exsnrex  3784  snprc  3807  euabsn2  3811  reusn  3813  eusn  3816  elunirab  3963  unipr  3964  uniun  3969  uniin  3970  uni0b  3975  uniintsn  4022  iuncom4  4035  dfiun2g  4058  iunn0  4085  iunxiun  4107  disjor  4130  cbvopab2  4213  cbvopab2v  4216  unopab  4218  axrep1  4255  axrep4  4258  axrep5  4259  zfrep4  4262  axsep  4263  zfnuleu  4269  axnulALT  4270  0ex  4273  vprc  4275  inex1  4278  inuni  4296  axpweq  4310  zfpow  4312  axpow2  4313  axpow3  4314  pwex  4316  zfpair  4335  zfpair2  4338  eqvinop  4375  copsexg  4376  opabn0  4419  iunopab  4420  dfid3  4433  zfun  4635  uniex2  4637  uniuni  4649  reusv5OLD  4666  elxp2  4829  opeliunxp  4862  xpiundi  4865  xpiundir  4866  elvvv  4870  eliunxp  4945  relop  4956  opelco2g  4973  cnvco  4989  cnvuni  4990  dfdm3  4991  dfrn2  4992  dfrn3  4993  elrng  4995  dfdm4  4996  eldm2g  4999  dmun  5009  dmin  5010  dmiun  5011  dmuni  5012  dmopab  5013  dmi  5017  elrn  5043  rnopab  5048  dmcosseq  5070  dmres  5100  elres  5114  elsnres  5115  dfima2  5138  elima3  5143  imadmrn  5148  imai  5151  args  5165  rniun  5215  ssrnres  5242  dmsnn0  5268  dmsnopg  5274  elxp4  5290  elxp5  5291  cnvresima  5292  mptpreima  5296  dfco2  5302  coundi  5304  coundir  5305  resco  5307  imaco  5308  rnco  5309  coiun  5312  coi1  5318  coass  5321  xpco  5347  dffun2  5397  dffun5  5400  imadif  5461  funimaexg  5463  fun11iun  5628  f11o  5641  brprcneu  5654  dffv2  5728  fndmin  5769  fvresex  5914  abrexco  5918  opabex3d  5921  opabex3  5922  imaiun  5924  abexssex  5934  abexex  5935  isomin  5989  dfoprab2  6053  cbvoprab2  6077  oprabrexex2  6121  releldm2  6329  dfopab2  6333  dfoprab3s  6334  exopxfr  6342  fsplit  6383  frxp  6385  brtpos2  6414  oarec  6734  oeeu  6775  domen  7050  mapsnen  7113  xpsnen  7121  xpcomco  7127  xpassen  7131  inf2  7504  zfinf  7520  axinf2  7521  zfinf2  7523  rankuni  7715  scott0  7736  cp  7741  ween  7842  aceq1  7924  aceq0  7925  aceq2  7926  dfac5lem1  7930  dfac5lem2  7931  dfac5lem3  7932  kmlem3  7958  kmlem14  7969  kmlem15  7970  kmlem16  7971  cflem  8052  cf0  8057  cfval2  8066  cfss  8071  cfslb  8072  fin23lem32  8150  axdc2lem  8254  zfac  8266  ac9  8289  ac9s  8299  axpowndlem3  8400  zfcndrep  8415  zfcndun  8416  zfcndpow  8417  zfcndinf  8419  zfcndac  8420  axgroth5  8625  axgroth2  8626  grothpw  8627  axgroth6  8629  axgroth3  8632  axgroth4  8633  grothprim  8635  grothtsk  8636  genpass  8812  ltexprlem1  8839  ltexprlem4  8842  supmul1  9898  supmullem2  9900  2rexuz  10454  nnwos  10469  hashfun  11620  maxprmfct  13033  4sqlem12  13244  vdwmc  13266  imasleval  13686  isacs2  13798  gsumval3eu  15433  lidlnz  16219  isbasis2g  16929  tgval2  16937  ntreq0  17057  lmff  17280  cmpfi  17386  is1stc2  17419  1stcelcls  17438  isfbas2  17781  elfg  17817  alexsubALTlem3  17994  ustfilxp  18156  metrest  18437  metuel2  18478  restmetu  18482  cmetss  19131  dchrvmasumlema  21054  usgraedg4  21265  3v3e3cycl2  21492  isgrpo  21625  ismgm  21749  nmo  23810  2reuswap2  23812  rexunirn  23815  disjorf  23858  axextprim  24922  axrepprim  24923  axunprim  24924  axpowprim  24925  axregprim  24926  axinfprim  24927  axacprim  24928  cbvprod  25013  iprodmul  25081  dftr6  25124  coep  25125  coepr  25126  dffr5  25127  dfpo2  25129  cnvco1  25134  cnvco2  25135  eldm3  25136  fundmpss  25139  dfdm5  25149  dfrn5  25150  domep  25166  axextdfeq  25171  19.12b  25175  axextndbi  25178  wfrlem11  25283  tfrALTlem  25293  frrlem5c  25304  nofulllem5  25377  brtxp  25437  brpprod  25442  brsset  25446  dfon3  25449  brtxpsd  25451  elfix  25460  dffix2  25462  dffun10  25470  elfuns  25471  elsingles  25474  snelsingles  25478  dfiota3  25479  brimg  25493  brapply  25494  brcup  25495  brcap  25496  brsuccf  25497  funpartlem  25498  brrestrict  25505  dfrdg4  25506  tfrqfree  25507  supaddc  25940  supadd  25941  itg2addnc  25952  neifg  26084  prtlem16  26402  prter2  26414  diophrex  26518  19.36vv  27243  19.37vv  27245  pm11.58  27251  pm11.6  27253  pm13.192  27272  2sbc5g  27278  iotasbc2  27282  rfcnnnub  27368  stoweidlem34  27444  stoweidlem35  27445  stoweidlem60  27470  rmoanim  27618  2rmoswap  27623  frgrawopreglem2  27790  onfrALTlem5  27964  onfrALTlem1  27970  a9e2nd  27981  2sb5nd  27983  en3lplem2VD  28290  relopabVD  28347  a9e2ndVD  28354  2sb5ndVD  28356  a9e2ndALT  28377  2sb5ndALT  28379  bnj89  28417  bnj133  28423  bnj1019  28481  bnj1101  28486  bnj1109  28488  bnj1143  28492  bnj1198  28498  bnj1304  28522  bnj605  28609  bnj607  28618  bnj600  28621  bnj865  28625  bnj916  28635  bnj983  28653  bnj985  28655  bnj996  28657  bnj1033  28669  bnj1083  28678  bnj1090  28679  bnj1093  28680  bnj1110  28682  bnj1128  28690  bnj1145  28693  bnj1171  28700  bnj1172  28701  bnj1174  28703  bnj1176  28705  bnj1186  28707  bnj1189  28709  bnj1253  28717  bnj1279  28718  bnj1371  28729  bnj1374  28731  bnj1312  28758  equsexNEW7  28821  exsbOLDNEW7  28926  2sb5NEW7  28935  sbel2xNEW7  28940  excom13OLD7  29004  exrot4OLD7  29006  eeorOLD7  29008  19.12vvOLD7  29010  eeanOLD7  29011  eeeanvOLD7  29013  ee4anvOLD7  29014  2sb5rfOLD7  29071  2exsbOLD7  29077  equsexv-x12  29089  equvinv  29090  islshpat  29183  islpln5  29700  islvol5  29744  pmapglb  29935  polval2N  30071  cdlemftr3  30730  dibelval3  31313  dicelval3  31346  dihglb2  31508
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563
This theorem depends on definitions:  df-bi 178  df-ex 1548
  Copyright terms: Public domain W3C validator