Theorem exbii 1541

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

Step	Hyp	Ref	Expression
1		exbi 1540	. 2 |- ( A. x ( ph <-> ps ) -> ( E. x ph <-> E. x ps ) )
2		exbii.1	. 2 |- ( ph <-> ps )
3	1, 2	mpg 1385	1 |- ( E. x ph <-> E. x ps )

Syntax hints:   <-> wb 103   E.wex 1426

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-ial 1472

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  2exbii  1542  3exbii  1543  exancom  1544  excom13  1624  exrot4  1626  eeor  1630  sbcof2  1738  sbequ8  1775  sbidm  1779  sborv  1818  19.41vv  1831  19.41vvv  1832  19.41vvvv  1833  exdistr  1835  19.42vvv  1837  exdistr2  1839  3exdistr  1840  4exdistr  1841  eean  1854  eeeanv  1856  ee4anv  1857  2sb5  1907  2sb5rf  1913  sbel2x  1922  sbexyz  1927  sbex  1928  exsb  1932  2exsb  1933  sb8eu  1961  sb8euh  1971  eu1  1973  eu2  1992  2moswapdc  2038  2exeu  2040  exists1  2044  clelab  2212  clabel  2213  sbabel  2254  rexbii2  2389  r2exf  2396  nfrexdya  2413  r19.41  2522  r19.43  2525  isset  2625  rexv  2637  ceqsex2  2659  ceqsex3v  2661  gencbvex  2665  ceqsrexv  2747  rexab  2777  rexrab2  2782  euxfrdc  2801  euind  2802  reu6  2804  reu3  2805  2reuswapdc  2819  reuind  2820  sbccomlem  2913  rmo2ilem  2928  rexun  3180  reupick3  3284  abn0r  3307  abn0m  3308  rabn0m  3310  rexsns  3482  exsnrex  3485  snprc  3507  euabsn2  3511  reusn  3513  eusn  3516  elunirab  3666  unipr  3667  uniun  3672  uniin  3673  iuncom4  3737  dfiun2g  3762  iunn0m  3790  iunxiun  3810  disjnim  3836  cbvopab2  3912  cbvopab2v  3915  unopab  3917  zfnuleu  3963  0ex  3966  vnex  3970  inex1  3973  intexabim  3988  iinexgm  3990  inuni  3991  unidif0  4002  axpweq  4006  zfpow  4010  axpow2  4011  axpow3  4012  vpwex  4014  zfpair2  4037  mss  4053  exss  4054  opm  4061  eqvinop  4070  copsexg  4071  opabm  4107  iunopab  4108  zfun  4261  uniex2  4263  uniuni  4273  rexxfrd  4285  dtruex  4375  zfinf2  4404  elxp2  4456  opeliunxp  4493  xpiundi  4496  xpiundir  4497  elvvv  4501  eliunxp  4575  rexiunxp  4578  relop  4586  elco  4602  opelco2g  4604  cnvco  4621  cnvuni  4622  dfdm3  4623  dfrn2  4624  dfrn3  4625  elrng  4627  dfdm4  4628  eldm2g  4632  dmun  4643  dmin  4644  dmiun  4645  dmuni  4646  dmopab  4647  dmi  4651  dmmrnm  4655  elrn  4678  rnopab  4682  dmcosseq  4704  dmres  4734  elres  4748  elsnres  4749  dfima2  4776  elima3  4781  imadmrn  4784  imai  4788  args  4801  rniun  4842  ssrnres  4873  dmsnm  4896  dmsnopg  4902  elxp4  4918  elxp5  4919  cnvresima  4920  mptpreima  4924  dfco2  4930  coundi  4932  coundir  4933  resco  4935  imaco  4936  rnco  4937  coiun  4940  coi1  4946  coass  4949  xpcom  4977  dffun2  5025  imadif  5094  imainlem  5095  funimaexglem  5097  fun11iun  5274  f11o  5286  brprcneu  5298  nfvres  5337  fndmin  5406  abrexco  5538  imaiun  5539  dfoprab2  5696  cbvoprab2  5721  rexrnmpt2  5760  opabex3d  5892  opabex3  5893  abexssex  5896  abexex  5897  oprabrexex2  5901  releldm2  5955  dfopab2  5959  dfoprab3s  5960  cnvoprab  5999  brtpos2  6016  tfr1onlemaccex  6113  tfrcllembxssdm  6121  tfrcllemaccex  6126  domen  6468  mapsnen  6528  xpsnen  6537  xpcomco  6542  xpassen  6546  fimax2gtri  6617  supelti  6697  subhalfnqq  6973  ltbtwnnq  6975  prnmaxl  7047  prnminu  7048  prarloc  7062  genpdflem  7066  genpassl  7083  genpassu  7084  ltexprlemm  7159  2rexuz  9070  seq3f1olemp  9931  cbvsum  10749  bj-axempty  11784  bj-axempty2  11785  bj-vprc  11787  bdinex1  11790  bj-zfpair2  11801  bj-uniex2  11807  bj-d0clsepcl  11820