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  5604  f11o  5617  brprcneu  5632  nfvres  5675  fndmin  5754  abrexco  5900  imaiun  5901  dfoprab2  6068  cbvoprab2  6094  rexrnmpo  6137  opabex3d  6283  opabex3  6284  abexssex  6287  abexex  6288  oprabrexex2  6292  uchoice  6300  releldm2  6348  dfopab2  6352  dfoprab3s  6353  cnvoprab  6399  brtpos2  6417  tfr1onlemaccex  6514  tfrcllembxssdm  6522  tfrcllemaccex  6527  domen  6922  mapsnen  6986  xpsnen  7005  xpcomco  7010  xpassen  7014  fimax2gtri  7091  supelti  7201  cc1  7484  subhalfnqq  7634  ltbtwnnq  7636  prnmaxl  7708  prnminu  7709  prarloc  7723  genpdflem  7727  genpassl  7744  genpassu  7745  ltexprlemm  7820  2rexuz  9816  seq3f1olemp  10777  cbvsum  11921  cbvprod  12120  nnwosdc  12611  4sqlem12  12976  inffinp1  13051  ctiunctal  13063  unct  13064  isbasis2g  14771  tgval2  14777  ntreq0  14858  lmff  14975  metrest  15232  upgrex  15956  1loopgrvd2fi  16158  bj-axempty  16491  bj-axempty2  16492  bj-vprc  16494  bdinex1  16497  bj-zfpair2  16508  bj-uniex2  16514  bj-d0clsepcl  16523