Theorem exbii 1653

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

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

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-ial 1582

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2exbii  1654  3exbii  1655  exancom  1656  excom13  1737  exrot4  1739  eeor  1743  sbcof2  1858  sbequ8  1895  sbidm  1899  sborv  1939  19.41vv  1952  19.41vvv  1953  19.41vvvv  1954  exdistr  1958  19.42vvv  1961  exdistr2  1963  3exdistr  1964  4exdistr  1965  eean  1984  eeeanv  1986  ee4anv  1987  2sb5  2036  2sb5rf  2042  sbel2x  2051  sbexyz  2056  sbex  2057  exsb  2061  2exsb  2062  sb8eu  2092  sb8euh  2102  eu1  2104  eu2  2124  2moswapdc  2170  2exeu  2172  exists1  2176  clelab  2357  clabel  2358  sbabel  2401  rexbii2  2543  r2exf  2550  nfrexdya  2568  r19.41  2688  r19.43  2691  cbvreuvw  2773  isset  2809  rexv  2821  ceqsex2  2844  ceqsex3v  2846  gencbvex  2850  ceqsrexv  2936  rexab  2968  rexrab2  2973  euxfrdc  2992  euind  2993  reu6  2995  reu3  2996  2reuswapdc  3010  reuind  3011  sbccomlem  3106  rmo2ilem  3122  rexun  3387  reupick3  3492  abn0r  3519  abn0m  3520  rabn0m  3522  rexsns  3708  exsnrex  3711  snprc  3734  euabsn2  3740  reusn  3742  eusn  3745  snmb  3793  elunirab  3906  unipr  3907  uniun  3912  uniin  3913  iuncom4  3977  dfiun2g  4002  iunn0m  4031  iunxiun  4052  disjnim  4078  cbvopab2  4163  cbvopab2v  4166  unopab  4168  zfnuleu  4213  0ex  4216  vnex  4220  inex1  4223  intexabim  4242  iinexgm  4244  inuni  4245  unidif0  4257  axpweq  4261  zfpow  4265  axpow2  4266  axpow3  4267  vpwex  4269  zfpair2  4300  mss  4318  exss  4319  opm  4326  eqvinop  4335  copsexg  4336  opabm  4375  iunopab  4376  zfun  4531  uniex2  4533  uniuni  4548  rexxfrd  4560  dtruex  4657  zfinf2  4687  elxp2  4743  opeliunxp  4781  xpiundi  4784  xpiundir  4785  elvvv  4789  eliunxp  4869  rexiunxp  4872  relop  4880  elco  4896  opelco2g  4898  cnvco  4915  cnvuni  4916  dfdm3  4917  dfrn2  4918  dfrn3  4919  elrng  4921  dfdm4  4923  eldm2g  4927  dmun  4938  dmin  4939  dmiun  4940  dmuni  4941  dmopab  4942  dmi  4946  reldmm  4950  dmmrnm  4951  elrn  4975  rnopab  4979  dmcosseq  5004  dmres  5034  elres  5049  elsnres  5050  dfima2  5078  elima3  5083  imadmrn  5086  imai  5092  args  5105  rniun  5147  ssrnres  5179  dmsnm  5202  dmsnopg  5208  elxp4  5224  elxp5  5225  cnvresima  5226  mptpreima  5230  dfco2  5236  coundi  5238  coundir  5239  resco  5241  imaco  5242  rnco  5243  coiun  5246  coi1  5252  coass  5255  xpcom  5283  dffun2  5336  imadif  5410  imainlem  5411  funimaexglem  5413  fun11iun  5605  f11o  5618  brprcneu  5633  nfvres  5676  fndmin  5755  abrexco  5903  imaiun  5904  dfoprab2  6071  cbvoprab2  6097  rexrnmpo  6140  opabex3d  6286  opabex3  6287  abexssex  6290  abexex  6291  oprabrexex2  6295  uchoice  6303  releldm2  6351  dfopab2  6355  dfoprab3s  6356  cnvoprab  6402  brtpos2  6420  tfr1onlemaccex  6517  tfrcllembxssdm  6525  tfrcllemaccex  6530  domen  6925  mapsnen  6989  xpsnen  7008  xpcomco  7013  xpassen  7017  fimax2gtri  7094  supelti  7204  cc1  7487  subhalfnqq  7637  ltbtwnnq  7639  prnmaxl  7711  prnminu  7712  prarloc  7726  genpdflem  7730  genpassl  7747  genpassu  7748  ltexprlemm  7823  2rexuz  9819  seq3f1olemp  10781  cbvsum  11941  cbvprod  12140  nnwosdc  12631  4sqlem12  12996  inffinp1  13071  ctiunctal  13083  unct  13084  isbasis2g  14796  tgval2  14802  ntreq0  14883  lmff  15000  metrest  15257  upgrex  15981  1loopgrvd2fi  16183  bj-axempty  16547  bj-axempty2  16548  bj-vprc  16550  bdinex1  16553  bj-zfpair2  16564  bj-uniex2  16570  bj-d0clsepcl  16579