Theorem exbii 1658

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

This proof depends on syntax axioms:   <-> wb 105   E.wex 1545

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-ial 1587

This proof depends on definitions:  df-bi 117

This theorem is used by:  2exbii  1659  3exbii  1660  exancom  1661  excom13  1741  exrot4  1743  eeor  1747  sbcof2  1863  sbequ8  1900  sbidm  1904  sborv  1945  19.41vv  1959  19.41vvv  1960  19.41vvvv  1961  exdistr  1965  19.42vvv  1968  exdistr2  1970  3exdistr  1971  4exdistr  1972  eean  1991  eeeanv  1993  ee4anv  1994  2sb5  2043  2sb5rf  2049  sbel2x  2058  sbexyz  2063  sbex  2064  exsb  2068  2exsb  2069  sb8eu  2099  sb8euh  2109  eu1  2111  eu2  2131  2moswapdc  2177  2exeu  2179  exists1  2183  clelab  2366  clabel  2367  sbabel  2419  rexbii2  2561  r2exf  2568  nfrexdya  2586  r19.41  2706  r19.43  2709  cbvreuvw  2792  isset  2828  rexv  2840  ceqsex2  2863  ceqsex3v  2865  gencbvex  2869  ceqsrexv  2956  rexab  2988  rexrab2  2993  euxfrdc  3012  euind  3013  reu6  3015  reu3  3016  2reuswapdc  3030  reuind  3031  sbccomlem  3126  rmo2ilem  3142  rexun  3409  reupick3  3518  abn0r  3546  abn0m  3547  rabn0m  3549  rexsns  3748  exsnrex  3751  snprc  3774  euabsn2  3780  reusn  3782  eusn  3785  snmb  3834  elunirab  3948  unipr  3949  uniun  3954  uniin  3955  iuncom4  4019  dfiun2g  4044  iunn0m  4073  iunxiun  4094  disjnim  4120  cbvopab2  4206  cbvopab2v  4209  unopab  4211  zfnuleu  4259  0ex  4262  vnex  4266  inex1  4269  intexabim  4290  iinexgm  4292  inuni  4293  unidif0  4306  axpweq  4310  zfpow  4314  axpow2  4315  axpow3  4316  vpwex  4318  zfpair2  4349  mss  4368  exss  4369  opm  4376  eqvinop  4385  copsexg  4386  opabm  4425  iunopab  4426  zfun  4581  uniex2  4583  uniex2OLD  4584  uniuni  4599  rexxfrd  4611  dtruex  4708  zfinf2  4738  elxp2  4794  opeliunxp  4832  xpiundi  4835  xpiundir  4836  elvvv  4840  eliunxp  4921  rexiunxp  4924  relop  4932  elco  4948  opelco2g  4950  cnvco  4967  cnvuni  4968  dfdm3  4969  dfrn2  4970  dfrn3  4971  elrng  4973  dfdm4  4975  eldm2g  4979  dmun  4990  dmin  4991  dmiun  4992  dmuni  4993  dmopab  4994  dmi  4998  reldmm  5002  dmmrnm  5003  elrn  5027  rnopab  5031  dmcosseq  5056  dmres  5086  elres  5101  elsnres  5102  dfima2  5131  elima3  5136  imadmrn  5139  imai  5146  args  5159  rniun  5201  ssrnres  5233  dmsnm  5256  dmsnopg  5262  elxp4  5278  elxp5  5279  cnvresima  5280  mptpreima  5284  dfco2  5290  coundi  5292  coundir  5293  resco  5295  imaco  5296  rnco  5297  coiun  5300  coi1  5306  coass  5309  xpcom  5337  dffun2  5390  imadif  5464  imainlem  5465  funimaexglem  5467  fun11iun  5663  f11o  5676  brprcneu  5691  nfvres  5735  fndmin  5819  abrexco  5968  imaiun  5969  dfoprab2  6138  cbvoprab2  6164  rexrnmpo  6207  opabex3d  6354  opabex3  6355  abexssex  6358  abexex  6359  oprabrexex2  6367  uchoice  6375  releldm2  6423  dfopab2  6427  dfoprab3s  6428  cnvoprab  6474  cnvimadfsn  6489  brtpos2  6526  tfr1onlemaccex  6623  tfrcllembxssdm  6631  tfrcllemaccex  6636  domen  7039  mapsnen  7104  xpsnen  7123  xpcomco  7128  xpassen  7132  fimax2gtri  7210  supelti  7348  cc1  7637  subhalfnqq  7787  ltbtwnnq  7789  prnmaxl  7861  prnminu  7862  prarloc  7876  genpdflem  7880  genpassl  7897  genpassu  7898  ltexprlemm  7973  2rexuz  9998  seq3f1olemp  10973  cbvsum  12151  cbvprod  12350  nnwosdc  12841  4sqlem12  13210  inffinp1  13378  ctiunctal  13390  unct  13391  isbasis2g  15271  tgval2  15277  ntreq0  15358  lmff  15475  metrest  15732  upgrex  16549  1loopgrvd2fi  16751  bj-axempty  17124  bj-axempty2  17125  bj-vprc  17127  bdinex1  17130  bj-zfpair2  17141  bj-uniex2  17147  bj-d0clsepcl  17156  wexmiddifxylem  17250  alsbii  17348