Theorem exbii 1628

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

Syntax hints:   <-> wb 105   E.wex 1515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-ial 1557

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2exbii  1629  3exbii  1630  exancom  1631  excom13  1712  exrot4  1714  eeor  1718  sbcof2  1833  sbequ8  1870  sbidm  1874  sborv  1914  19.41vv  1927  19.41vvv  1928  19.41vvvv  1929  exdistr  1933  19.42vvv  1936  exdistr2  1938  3exdistr  1939  4exdistr  1940  eean  1959  eeeanv  1961  ee4anv  1962  2sb5  2011  2sb5rf  2017  sbel2x  2026  sbexyz  2031  sbex  2032  exsb  2036  2exsb  2037  sb8eu  2067  sb8euh  2077  eu1  2079  eu2  2098  2moswapdc  2144  2exeu  2146  exists1  2150  clelab  2331  clabel  2332  sbabel  2375  rexbii2  2517  r2exf  2524  nfrexdya  2542  r19.41  2661  r19.43  2664  cbvreuvw  2744  isset  2778  rexv  2790  ceqsex2  2813  ceqsex3v  2815  gencbvex  2819  ceqsrexv  2903  rexab  2935  rexrab2  2940  euxfrdc  2959  euind  2960  reu6  2962  reu3  2963  2reuswapdc  2977  reuind  2978  sbccomlem  3073  rmo2ilem  3088  rexun  3353  reupick3  3458  abn0r  3485  abn0m  3486  rabn0m  3488  rexsns  3672  exsnrex  3675  snprc  3698  euabsn2  3702  reusn  3704  eusn  3707  elunirab  3863  unipr  3864  uniun  3869  uniin  3870  iuncom4  3934  dfiun2g  3959  iunn0m  3988  iunxiun  4009  disjnim  4035  cbvopab2  4119  cbvopab2v  4122  unopab  4124  zfnuleu  4169  0ex  4172  vnex  4176  inex1  4179  intexabim  4197  iinexgm  4199  inuni  4200  unidif0  4212  axpweq  4216  zfpow  4220  axpow2  4221  axpow3  4222  vpwex  4224  zfpair2  4255  mss  4271  exss  4272  opm  4279  eqvinop  4288  copsexg  4289  opabm  4328  iunopab  4329  zfun  4482  uniex2  4484  uniuni  4499  rexxfrd  4511  dtruex  4608  zfinf2  4638  elxp2  4694  opeliunxp  4731  xpiundi  4734  xpiundir  4735  elvvv  4739  eliunxp  4818  rexiunxp  4821  relop  4829  elco  4845  opelco2g  4847  cnvco  4864  cnvuni  4865  dfdm3  4866  dfrn2  4867  dfrn3  4868  elrng  4870  dfdm4  4871  eldm2g  4875  dmun  4886  dmin  4887  dmiun  4888  dmuni  4889  dmopab  4890  dmi  4894  dmmrnm  4898  elrn  4922  rnopab  4926  dmcosseq  4951  dmres  4981  elres  4996  elsnres  4997  dfima2  5025  elima3  5030  imadmrn  5033  imai  5039  args  5052  rniun  5094  ssrnres  5126  dmsnm  5149  dmsnopg  5155  elxp4  5171  elxp5  5172  cnvresima  5173  mptpreima  5177  dfco2  5183  coundi  5185  coundir  5186  resco  5188  imaco  5189  rnco  5190  coiun  5193  coi1  5199  coass  5202  xpcom  5230  dffun2  5282  imadif  5355  imainlem  5356  funimaexglem  5358  fun11iun  5545  f11o  5557  brprcneu  5571  nfvres  5612  fndmin  5689  abrexco  5830  imaiun  5831  dfoprab2  5994  cbvoprab2  6020  rexrnmpo  6063  opabex3d  6208  opabex3  6209  abexssex  6212  abexex  6213  oprabrexex2  6217  uchoice  6225  releldm2  6273  dfopab2  6277  dfoprab3s  6278  cnvoprab  6322  brtpos2  6339  tfr1onlemaccex  6436  tfrcllembxssdm  6444  tfrcllemaccex  6449  domen  6842  mapsnen  6905  xpsnen  6918  xpcomco  6923  xpassen  6927  fimax2gtri  7000  supelti  7106  cc1  7379  subhalfnqq  7529  ltbtwnnq  7531  prnmaxl  7603  prnminu  7604  prarloc  7618  genpdflem  7622  genpassl  7639  genpassu  7640  ltexprlemm  7715  2rexuz  9705  seq3f1olemp  10662  cbvsum  11704  cbvprod  11902  nnwosdc  12393  4sqlem12  12758  inffinp1  12833  ctiunctal  12845  unct  12846  isbasis2g  14550  tgval2  14556  ntreq0  14637  lmff  14754  metrest  15011  bj-axempty  15866  bj-axempty2  15867  bj-vprc  15869  bdinex1  15872  bj-zfpair2  15883  bj-uniex2  15889  bj-d0clsepcl  15898