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  4118  cbvopab2v  4121  unopab  4123  zfnuleu  4168  0ex  4171  vnex  4175  inex1  4178  intexabim  4196  iinexgm  4198  inuni  4199  unidif0  4211  axpweq  4215  zfpow  4219  axpow2  4220  axpow3  4221  vpwex  4223  zfpair2  4254  mss  4270  exss  4271  opm  4278  eqvinop  4287  copsexg  4288  opabm  4327  iunopab  4328  zfun  4481  uniex2  4483  uniuni  4498  rexxfrd  4510  dtruex  4607  zfinf2  4637  elxp2  4693  opeliunxp  4730  xpiundi  4733  xpiundir  4734  elvvv  4738  eliunxp  4817  rexiunxp  4820  relop  4828  elco  4844  opelco2g  4846  cnvco  4863  cnvuni  4864  dfdm3  4865  dfrn2  4866  dfrn3  4867  elrng  4869  dfdm4  4870  eldm2g  4874  dmun  4885  dmin  4886  dmiun  4887  dmuni  4888  dmopab  4889  dmi  4893  dmmrnm  4897  elrn  4921  rnopab  4925  dmcosseq  4950  dmres  4980  elres  4995  elsnres  4996  dfima2  5024  elima3  5029  imadmrn  5032  imai  5038  args  5051  rniun  5093  ssrnres  5125  dmsnm  5148  dmsnopg  5154  elxp4  5170  elxp5  5171  cnvresima  5172  mptpreima  5176  dfco2  5182  coundi  5184  coundir  5185  resco  5187  imaco  5188  rnco  5189  coiun  5192  coi1  5198  coass  5201  xpcom  5229  dffun2  5281  imadif  5354  imainlem  5355  funimaexglem  5357  fun11iun  5543  f11o  5555  brprcneu  5569  nfvres  5610  fndmin  5687  abrexco  5828  imaiun  5829  dfoprab2  5992  cbvoprab2  6018  rexrnmpo  6061  opabex3d  6206  opabex3  6207  abexssex  6210  abexex  6211  oprabrexex2  6215  uchoice  6223  releldm2  6271  dfopab2  6275  dfoprab3s  6276  cnvoprab  6320  brtpos2  6337  tfr1onlemaccex  6434  tfrcllembxssdm  6442  tfrcllemaccex  6447  domen  6840  mapsnen  6903  xpsnen  6916  xpcomco  6921  xpassen  6925  fimax2gtri  6998  supelti  7104  cc1  7377  subhalfnqq  7527  ltbtwnnq  7529  prnmaxl  7601  prnminu  7602  prarloc  7616  genpdflem  7620  genpassl  7637  genpassu  7638  ltexprlemm  7713  2rexuz  9703  seq3f1olemp  10660  cbvsum  11671  cbvprod  11869  nnwosdc  12360  4sqlem12  12725  inffinp1  12800  ctiunctal  12812  unct  12813  isbasis2g  14517  tgval2  14523  ntreq0  14604  lmff  14721  metrest  14978  bj-axempty  15829  bj-axempty2  15830  bj-vprc  15832  bdinex1  15835  bj-zfpair2  15846  bj-uniex2  15852  bj-d0clsepcl  15861