Theorem exbii 1585

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 1584	. 2 |- ( A. x ( ph <-> ps ) -> ( E. x ph <-> E. x ps ) )
2		exbii.1	. 2 |- ( ph <-> ps )
3	1, 2	mpg 1428	1 |- ( E. x ph <-> E. x ps )

Syntax hints:   <-> wb 104   E.wex 1469

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-ial 1515

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  2exbii  1586  3exbii  1587  exancom  1588  excom13  1668  exrot4  1670  eeor  1674  sbcof2  1783  sbequ8  1820  sbidm  1824  sborv  1863  19.41vv  1876  19.41vvv  1877  19.41vvvv  1878  exdistr  1882  19.42vvv  1885  exdistr2  1887  3exdistr  1888  4exdistr  1889  eean  1904  eeeanv  1906  ee4anv  1907  2sb5  1959  2sb5rf  1965  sbel2x  1974  sbexyz  1979  sbex  1980  exsb  1984  2exsb  1985  sb8eu  2013  sb8euh  2023  eu1  2025  eu2  2044  2moswapdc  2090  2exeu  2092  exists1  2096  clelab  2266  clabel  2267  sbabel  2308  rexbii2  2449  r2exf  2456  nfrexdya  2473  r19.41  2589  r19.43  2592  isset  2695  rexv  2707  ceqsex2  2729  ceqsex3v  2731  gencbvex  2735  ceqsrexv  2819  rexab  2850  rexrab2  2855  euxfrdc  2874  euind  2875  reu6  2877  reu3  2878  2reuswapdc  2892  reuind  2893  sbccomlem  2987  rmo2ilem  3002  rexun  3261  reupick3  3366  abn0r  3392  abn0m  3393  rabn0m  3395  rexsns  3570  exsnrex  3573  snprc  3596  euabsn2  3600  reusn  3602  eusn  3605  elunirab  3757  unipr  3758  uniun  3763  uniin  3764  iuncom4  3828  dfiun2g  3853  iunn0m  3881  iunxiun  3902  disjnim  3928  cbvopab2  4010  cbvopab2v  4013  unopab  4015  zfnuleu  4060  0ex  4063  vnex  4067  inex1  4070  intexabim  4085  iinexgm  4087  inuni  4088  unidif0  4099  axpweq  4103  zfpow  4107  axpow2  4108  axpow3  4109  vpwex  4111  zfpair2  4140  mss  4156  exss  4157  opm  4164  eqvinop  4173  copsexg  4174  opabm  4210  iunopab  4211  zfun  4364  uniex2  4366  uniuni  4380  rexxfrd  4392  dtruex  4482  zfinf2  4511  elxp2  4565  opeliunxp  4602  xpiundi  4605  xpiundir  4606  elvvv  4610  eliunxp  4686  rexiunxp  4689  relop  4697  elco  4713  opelco2g  4715  cnvco  4732  cnvuni  4733  dfdm3  4734  dfrn2  4735  dfrn3  4736  elrng  4738  dfdm4  4739  eldm2g  4743  dmun  4754  dmin  4755  dmiun  4756  dmuni  4757  dmopab  4758  dmi  4762  dmmrnm  4766  elrn  4790  rnopab  4794  dmcosseq  4818  dmres  4848  elres  4863  elsnres  4864  dfima2  4891  elima3  4896  imadmrn  4899  imai  4903  args  4916  rniun  4957  ssrnres  4989  dmsnm  5012  dmsnopg  5018  elxp4  5034  elxp5  5035  cnvresima  5036  mptpreima  5040  dfco2  5046  coundi  5048  coundir  5049  resco  5051  imaco  5052  rnco  5053  coiun  5056  coi1  5062  coass  5065  xpcom  5093  dffun2  5141  imadif  5211  imainlem  5212  funimaexglem  5214  fun11iun  5396  f11o  5408  brprcneu  5422  nfvres  5462  fndmin  5535  abrexco  5668  imaiun  5669  dfoprab2  5826  cbvoprab2  5852  rexrnmpo  5894  opabex3d  6027  opabex3  6028  abexssex  6031  abexex  6032  oprabrexex2  6036  releldm2  6091  dfopab2  6095  dfoprab3s  6096  cnvoprab  6139  brtpos2  6156  tfr1onlemaccex  6253  tfrcllembxssdm  6261  tfrcllemaccex  6266  domen  6653  mapsnen  6713  xpsnen  6723  xpcomco  6728  xpassen  6732  fimax2gtri  6803  supelti  6897  cc1  7097  subhalfnqq  7246  ltbtwnnq  7248  prnmaxl  7320  prnminu  7321  prarloc  7335  genpdflem  7339  genpassl  7356  genpassu  7357  ltexprlemm  7432  2rexuz  9404  seq3f1olemp  10306  cbvsum  11161  cbvprod  11359  inffinp1  11978  ctiunctal  11990  unct  11991  isbasis2g  12251  tgval2  12259  ntreq0  12340  lmff  12457  metrest  12714  bj-axempty  13262  bj-axempty2  13263  bj-vprc  13265  bdinex1  13268  bj-zfpair2  13279  bj-uniex2  13285  bj-d0clsepcl  13294