Theorem exbii 1542

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

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-4 1446  ax-ial 1473

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  2exbii  1543  3exbii  1544  exancom  1545  excom13  1625  exrot4  1627  eeor  1631  sbcof2  1739  sbequ8  1776  sbidm  1780  sborv  1819  19.41vv  1832  19.41vvv  1833  19.41vvvv  1834  exdistr  1836  19.42vvv  1838  exdistr2  1840  3exdistr  1841  4exdistr  1842  eean  1855  eeeanv  1857  ee4anv  1858  2sb5  1908  2sb5rf  1914  sbel2x  1923  sbexyz  1928  sbex  1929  exsb  1933  2exsb  1934  sb8eu  1962  sb8euh  1972  eu1  1974  eu2  1993  2moswapdc  2039  2exeu  2041  exists1  2045  clelab  2213  clabel  2214  sbabel  2255  rexbii2  2390  r2exf  2397  nfrexdya  2414  r19.41  2523  r19.43  2526  isset  2626  rexv  2638  ceqsex2  2660  ceqsex3v  2662  gencbvex  2666  ceqsrexv  2748  rexab  2778  rexrab2  2783  euxfrdc  2802  euind  2803  reu6  2805  reu3  2806  2reuswapdc  2820  reuind  2821  sbccomlem  2914  rmo2ilem  2929  rexun  3181  reupick3  3285  abn0r  3311  abn0m  3312  rabn0m  3314  rexsns  3486  exsnrex  3489  snprc  3511  euabsn2  3515  reusn  3517  eusn  3520  elunirab  3672  unipr  3673  uniun  3678  uniin  3679  iuncom4  3743  dfiun2g  3768  iunn0m  3796  iunxiun  3816  disjnim  3842  cbvopab2  3918  cbvopab2v  3921  unopab  3923  zfnuleu  3969  0ex  3972  vnex  3976  inex1  3979  intexabim  3994  iinexgm  3996  inuni  3997  unidif0  4008  axpweq  4012  zfpow  4016  axpow2  4017  axpow3  4018  vpwex  4020  zfpair2  4046  mss  4062  exss  4063  opm  4070  eqvinop  4079  copsexg  4080  opabm  4116  iunopab  4117  zfun  4270  uniex2  4272  uniuni  4286  rexxfrd  4298  dtruex  4388  zfinf2  4417  elxp2  4470  opeliunxp  4506  xpiundi  4509  xpiundir  4510  elvvv  4514  eliunxp  4588  rexiunxp  4591  relop  4599  elco  4615  opelco2g  4617  cnvco  4634  cnvuni  4635  dfdm3  4636  dfrn2  4637  dfrn3  4638  elrng  4640  dfdm4  4641  eldm2g  4645  dmun  4656  dmin  4657  dmiun  4658  dmuni  4659  dmopab  4660  dmi  4664  dmmrnm  4668  elrn  4691  rnopab  4695  dmcosseq  4717  dmres  4747  elres  4761  elsnres  4762  dfima2  4789  elima3  4794  imadmrn  4797  imai  4801  args  4814  rniun  4855  ssrnres  4886  dmsnm  4909  dmsnopg  4915  elxp4  4931  elxp5  4932  cnvresima  4933  mptpreima  4937  dfco2  4943  coundi  4945  coundir  4946  resco  4948  imaco  4949  rnco  4950  coiun  4953  coi1  4959  coass  4962  xpcom  4990  dffun2  5038  imadif  5107  imainlem  5108  funimaexglem  5110  fun11iun  5287  f11o  5299  brprcneu  5311  nfvres  5350  fndmin  5420  abrexco  5552  imaiun  5553  dfoprab2  5710  cbvoprab2  5735  rexrnmpt2  5774  opabex3d  5906  opabex3  5907  abexssex  5910  abexex  5911  oprabrexex2  5915  releldm2  5969  dfopab2  5973  dfoprab3s  5974  cnvoprab  6013  brtpos2  6030  tfr1onlemaccex  6127  tfrcllembxssdm  6135  tfrcllemaccex  6140  domen  6522  mapsnen  6582  xpsnen  6591  xpcomco  6596  xpassen  6600  fimax2gtri  6671  supelti  6751  subhalfnqq  7034  ltbtwnnq  7036  prnmaxl  7108  prnminu  7109  prarloc  7123  genpdflem  7127  genpassl  7144  genpassu  7145  ltexprlemm  7220  2rexuz  9131  seq3f1olemp  9992  cbvsum  10810  isbasis2g  11804  tgval2  11812  ntreq0  11893  bj-axempty  12057  bj-axempty2  12058  bj-vprc  12060  bdinex1  12063  bj-zfpair2  12074  bj-uniex2  12080  bj-d0clsepcl  12093