Theorem exbii 1654

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

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

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-ial 1583

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2exbii  1655  3exbii  1656  exancom  1657  excom13  1737  exrot4  1739  eeor  1743  sbcof2  1859  sbequ8  1896  sbidm  1900  sborv  1941  19.41vv  1955  19.41vvv  1956  19.41vvvv  1957  exdistr  1961  19.42vvv  1964  exdistr2  1966  3exdistr  1967  4exdistr  1968  eean  1987  eeeanv  1989  ee4anv  1990  2sb5  2039  2sb5rf  2045  sbel2x  2054  sbexyz  2059  sbex  2060  exsb  2064  2exsb  2065  sb8eu  2095  sb8euh  2105  eu1  2107  eu2  2127  2moswapdc  2173  2exeu  2175  exists1  2179  clelab  2362  clabel  2363  sbabel  2413  rexbii2  2555  r2exf  2562  nfrexdya  2580  r19.41  2700  r19.43  2703  cbvreuvw  2786  isset  2822  rexv  2834  ceqsex2  2857  ceqsex3v  2859  gencbvex  2863  ceqsrexv  2949  rexab  2981  rexrab2  2986  euxfrdc  3005  euind  3006  reu6  3008  reu3  3009  2reuswapdc  3023  reuind  3024  sbccomlem  3119  rmo2ilem  3135  rexun  3401  reupick3  3508  abn0r  3535  abn0m  3536  rabn0m  3538  rexsns  3730  exsnrex  3733  snprc  3756  euabsn2  3762  reusn  3764  eusn  3767  snmb  3815  elunirab  3929  unipr  3930  uniun  3935  uniin  3936  iuncom4  4000  dfiun2g  4025  iunn0m  4054  iunxiun  4075  disjnim  4101  cbvopab2  4186  cbvopab2v  4189  unopab  4191  zfnuleu  4236  0ex  4239  vnex  4243  inex1  4246  intexabim  4266  iinexgm  4268  inuni  4269  unidif0  4282  axpweq  4286  zfpow  4290  axpow2  4291  axpow3  4292  vpwex  4294  zfpair2  4325  mss  4344  exss  4345  opm  4352  eqvinop  4361  copsexg  4362  opabm  4401  iunopab  4402  zfun  4557  uniex2  4559  uniuni  4574  rexxfrd  4586  dtruex  4683  zfinf2  4713  elxp2  4769  opeliunxp  4807  xpiundi  4810  xpiundir  4811  elvvv  4815  eliunxp  4896  rexiunxp  4899  relop  4907  elco  4923  opelco2g  4925  cnvco  4942  cnvuni  4943  dfdm3  4944  dfrn2  4945  dfrn3  4946  elrng  4948  dfdm4  4950  eldm2g  4954  dmun  4965  dmin  4966  dmiun  4967  dmuni  4968  dmopab  4969  dmi  4973  reldmm  4977  dmmrnm  4978  elrn  5002  rnopab  5006  dmcosseq  5031  dmres  5061  elres  5076  elsnres  5077  dfima2  5105  elima3  5110  imadmrn  5113  imai  5120  args  5133  rniun  5175  ssrnres  5207  dmsnm  5230  dmsnopg  5236  elxp4  5252  elxp5  5253  cnvresima  5254  mptpreima  5258  dfco2  5264  coundi  5266  coundir  5267  resco  5269  imaco  5270  rnco  5271  coiun  5274  coi1  5280  coass  5283  xpcom  5311  dffun2  5364  imadif  5438  imainlem  5439  funimaexglem  5441  fun11iun  5637  f11o  5650  brprcneu  5665  nfvres  5708  fndmin  5787  abrexco  5934  imaiun  5935  dfoprab2  6102  cbvoprab2  6128  rexrnmpo  6171  opabex3d  6316  opabex3  6317  abexssex  6320  abexex  6321  oprabrexex2  6325  uchoice  6333  releldm2  6381  dfopab2  6385  dfoprab3s  6386  cnvoprab  6432  cnvimadfsn  6447  brtpos2  6484  tfr1onlemaccex  6581  tfrcllembxssdm  6589  tfrcllemaccex  6594  domen  6990  mapsnen  7055  xpsnen  7074  xpcomco  7079  xpassen  7083  fimax2gtri  7161  supelti  7295  cc1  7581  subhalfnqq  7731  ltbtwnnq  7733  prnmaxl  7805  prnminu  7806  prarloc  7820  genpdflem  7824  genpassl  7841  genpassu  7842  ltexprlemm  7917  2rexuz  9917  seq3f1olemp  10881  cbvsum  12049  cbvprod  12248  nnwosdc  12739  4sqlem12  13104  inffinp1  13197  ctiunctal  13209  unct  13210  isbasis2g  14927  tgval2  14933  ntreq0  15014  lmff  15131  metrest  15388  upgrex  16115  1loopgrvd2fi  16317  bj-axempty  16680  bj-axempty2  16681  bj-vprc  16683  bdinex1  16686  bj-zfpair2  16697  bj-uniex2  16703  bj-d0clsepcl  16712