Theorem exbii 1593

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

Syntax hints:   <-> wb 104   E.wex 1480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-ial 1522

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  2exbii  1594  3exbii  1595  exancom  1596  excom13  1677  exrot4  1679  eeor  1683  sbcof2  1798  sbequ8  1835  sbidm  1839  sborv  1878  19.41vv  1891  19.41vvv  1892  19.41vvvv  1893  exdistr  1897  19.42vvv  1900  exdistr2  1902  3exdistr  1903  4exdistr  1904  eean  1919  eeeanv  1921  ee4anv  1922  2sb5  1971  2sb5rf  1977  sbel2x  1986  sbexyz  1991  sbex  1992  exsb  1996  2exsb  1997  sb8eu  2027  sb8euh  2037  eu1  2039  eu2  2058  2moswapdc  2104  2exeu  2106  exists1  2110  clelab  2292  clabel  2293  sbabel  2335  rexbii2  2477  r2exf  2484  nfrexdya  2502  r19.41  2621  r19.43  2624  cbvreuvw  2698  isset  2732  rexv  2744  ceqsex2  2766  ceqsex3v  2768  gencbvex  2772  ceqsrexv  2856  rexab  2888  rexrab2  2893  euxfrdc  2912  euind  2913  reu6  2915  reu3  2916  2reuswapdc  2930  reuind  2931  sbccomlem  3025  rmo2ilem  3040  rexun  3302  reupick3  3407  abn0r  3433  abn0m  3434  rabn0m  3436  rexsns  3615  exsnrex  3618  snprc  3641  euabsn2  3645  reusn  3647  eusn  3650  elunirab  3802  unipr  3803  uniun  3808  uniin  3809  iuncom4  3873  dfiun2g  3898  iunn0m  3926  iunxiun  3947  disjnim  3973  cbvopab2  4056  cbvopab2v  4059  unopab  4061  zfnuleu  4106  0ex  4109  vnex  4113  inex1  4116  intexabim  4131  iinexgm  4133  inuni  4134  unidif0  4146  axpweq  4150  zfpow  4154  axpow2  4155  axpow3  4156  vpwex  4158  zfpair2  4188  mss  4204  exss  4205  opm  4212  eqvinop  4221  copsexg  4222  opabm  4258  iunopab  4259  zfun  4412  uniex2  4414  uniuni  4429  rexxfrd  4441  dtruex  4536  zfinf2  4566  elxp2  4622  opeliunxp  4659  xpiundi  4662  xpiundir  4663  elvvv  4667  eliunxp  4743  rexiunxp  4746  relop  4754  elco  4770  opelco2g  4772  cnvco  4789  cnvuni  4790  dfdm3  4791  dfrn2  4792  dfrn3  4793  elrng  4795  dfdm4  4796  eldm2g  4800  dmun  4811  dmin  4812  dmiun  4813  dmuni  4814  dmopab  4815  dmi  4819  dmmrnm  4823  elrn  4847  rnopab  4851  dmcosseq  4875  dmres  4905  elres  4920  elsnres  4921  dfima2  4948  elima3  4953  imadmrn  4956  imai  4960  args  4973  rniun  5014  ssrnres  5046  dmsnm  5069  dmsnopg  5075  elxp4  5091  elxp5  5092  cnvresima  5093  mptpreima  5097  dfco2  5103  coundi  5105  coundir  5106  resco  5108  imaco  5109  rnco  5110  coiun  5113  coi1  5119  coass  5122  xpcom  5150  dffun2  5198  imadif  5268  imainlem  5269  funimaexglem  5271  fun11iun  5453  f11o  5465  brprcneu  5479  nfvres  5519  fndmin  5592  abrexco  5727  imaiun  5728  dfoprab2  5889  cbvoprab2  5915  rexrnmpo  5957  opabex3d  6089  opabex3  6090  abexssex  6093  abexex  6094  oprabrexex2  6098  releldm2  6153  dfopab2  6157  dfoprab3s  6158  cnvoprab  6202  brtpos2  6219  tfr1onlemaccex  6316  tfrcllembxssdm  6324  tfrcllemaccex  6329  domen  6717  mapsnen  6777  xpsnen  6787  xpcomco  6792  xpassen  6796  fimax2gtri  6867  supelti  6967  cc1  7206  subhalfnqq  7355  ltbtwnnq  7357  prnmaxl  7429  prnminu  7430  prarloc  7444  genpdflem  7448  genpassl  7465  genpassu  7466  ltexprlemm  7541  2rexuz  9520  seq3f1olemp  10437  cbvsum  11301  cbvprod  11499  nnwosdc  11972  inffinp1  12362  ctiunctal  12374  unct  12375  isbasis2g  12693  tgval2  12701  ntreq0  12782  lmff  12899  metrest  13156  bj-axempty  13785  bj-axempty2  13786  bj-vprc  13788  bdinex1  13791  bj-zfpair2  13802  bj-uniex2  13808  bj-d0clsepcl  13817