Theorem exbii 1582

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.xph <-> E.xps)

Proof of Theorem exbii

Step	Hyp	Ref	Expression
1		exbi 1581	. 2 |- (A.x(ph <-> ps) -> (E.xph <-> E.xps))
2		exbii.1	. 2 |- (ph <-> ps)
3	1, 2	mpg 1548	1 |- (E.xph <-> E.xps)

Syntax hints:   <-> wb 176  E.wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557

This theorem depends on definitions:  df-bi 177  df-ex 1542

This theorem is referenced by:  2exbii  1583  3exbii  1584  exanali  1585  exancom  1586  19.43  1605  exiftruOLD  1658  excom  1741  excom13  1743  exrot4  1745  eeor  1885  19.12vv  1898  19.41vv  1902  19.41vvv  1903  19.41vvvv  1904  exdistr  1906  19.42vvv  1908  exdistr2  1909  3exdistr  1910  4exdistr  1911  eean  1912  eeeanv  1914  ee4anv  1915  equsex  1962  2sb5  2112  2sb5rf  2117  sbel2x  2125  exsbOLD  2131  2exsb  2132  sb8eu  2222  eu1  2225  eu2  2229  sbmo  2234  moanim  2260  2moswap  2279  2eu1  2284  exists1  2293  clelab  2474  clabel  2475  sbabel  2516  rexbii2  2644  r2exf  2651  r19.41  2764  isset  2864  rexv  2874  ceqsex2  2896  ceqsex3v  2898  gencbvex  2902  vtocl2  2911  vtocl3  2912  spc3gv  2945  ceqsrexv  2973  rexab  3000  rexrab2  3005  euxfr  3023  euind  3024  reu6  3026  reu3  3027  2reuswap  3039  reuind  3040  2reu5lem3  3044  2reu5  3045  sbccomlem  3117  rmo2  3132  rexun  3444  reupick3  3541  abn0  3569  pssnel  3616  rexsns  3765  snprc  3789  euabsn2  3792  reusn  3794  eusn  3797  elunirab  3905  unipr  3906  uniun  3911  uniin  3912  uni0b  3917  uniintsn  3964  iuncom4  3977  dfiun2g  4000  iunn0  4027  iunxiun  4049  axxpprim  4091  axcnvprim  4092  axssetprim  4093  axsiprim  4094  axtyplowerprim  4095  axins2prim  4096  axins3prim  4097  ninexg  4098  snex  4112  1cex  4143  elpw1  4145  elpw12  4146  elpw11c  4148  elpw121c  4149  elpw131c  4150  elpw141c  4151  elpw151c  4152  elpw161c  4153  elpw171c  4154  elpw181c  4155  elpw191c  4156  elpw1101c  4157  elpw1111c  4158  eluni1g  4173  otkelins2kg  4254  otkelins3kg  4255  opkelcokg  4262  opkelimagekg  4272  imacok  4283  xpkvexg  4286  dfimak2  4299  dfpw12  4302  insklem  4305  ndisjrelk  4324  unipw1  4326  dfpw2  4328  dfeu2  4334  dfaddc2  4382  dfnnc2  4396  elsuc  4414  addcass  4416  nnsucelrlem1  4425  preaddccan2lem1  4455  ltfinex  4465  ssfin  4471  eqpwrelk  4479  eqpw1relk  4480  ncfinraiselem2  4481  ncfinlowerlem1  4483  eqtfinrelk  4487  evenfinex  4504  oddfinex  4505  evenodddisjlem1  4516  nnadjoinlem1  4520  nnpweqlem1  4523  srelk  4525  sfintfinlem1  4532  tfinnnlem1  4534  spfinex  4538  vfinspsslem1  4551  vfinspss  4552  vfinncsp  4555  dfop2lem1  4574  eqvinop  4607  copsexg  4608  opeq  4620  cbvopab2  4634  cbvopab2v  4637  unopab  4639  opabn0  4717  el1st  4730  setconslem1  4732  setconslem2  4733  setconslem3  4734  setconslem4  4735  setconslem6  4737  setconslem7  4738  df1st2  4739  dfswap2  4742  dfco1  4749  dfid3  4769  elxp2  4803  xpiundi  4818  xpiundir  4819  opeliunxp  4821  eliunxp  4822  cnvco  4895  cnvuni  4896  elrn2  4898  eldm  4899  eldm2  4900  dfrn3  4904  dfrn4  4905  dmun  4913  dmin  4914  dmuni  4915  dmopab  4916  dmi  4920  elimapw1  4945  elimapw12  4946  elimapw13  4947  elimapw11c  4949  dfima3  4952  rnopab  4968  dmcoss  4972  dmcosseq  4974  dmres  4987  elsnres  4997  imadmrn  5009  imai  5011  rnuni  5039  ssrnres  5060  dmsnn0  5065  dmsnopg  5067  rnsnop  5076  cnvresima  5078  dfco2  5081  coundi  5083  coundir  5084  resco  5086  imaco  5087  rnco  5088  coiun  5091  coi1  5095  coass  5098  dfcnv2  5101  elxp4  5109  df2nd2  5112  dffun2  5120  dffun5  5123  nfunv  5139  imadif  5172  iunfopab  5205  fun11iun  5306  f11o  5316  dmfco  5382  abrexco  5464  imaiun  5465  funiunfv  5468  isomin  5497  opbr1st  5502  opbr2nd  5503  dfdm4  5508  dfrn5  5509  dmsi  5520  dfoprab2  5559  cbvoprab2  5569  mptpreima  5683  brsnsi1  5776  brsnsi2  5777  brco1st  5778  brco2nd  5779  trtxp  5782  elfix  5788  brimage  5794  oqelins4  5795  dmtxp  5803  txpcofun  5804  otsnelsi3  5806  releqel  5808  releqmpt2  5810  composeex  5821  disjex  5824  addcfnex  5825  funsex  5829  qrpprod  5837  brpprod  5840  dmpprod  5841  crossex  5851  pw1fnex  5853  pw1fnf1o  5856  fnfullfunlem1  5857  fvfullfunlem1  5862  domfnex  5871  ranfnex  5872  clos1ex  5877  transex  5911  refex  5912  antisymex  5913  connexex  5914  foundex  5915  extex  5916  symex  5917  frds  5936  ecdmn0  5968  qsexg  5983  enex  6032  xpassenlem  6057  xpassen  6058  enpw1lem1  6062  enmap2lem1  6064  enmap1lem1  6070  enpw1pw  6076  enprmaplem1  6077  nenpw1pwlem1  6085  lecex  6116  elncs  6120  ovmuc  6131  mucex  6134  ovcelem1  6172  ceexlem1  6174  ceex  6175  ce0nnul  6178  ce0addcnnul  6180  el2c  6192  taddc  6230  tcfnex  6245  csucex  6260  nnltp1clem1  6262  addccan2nclem1  6264  addccan2nclem2  6265  nmembers1lem1  6269  nncdiv3lem1  6276  nncdiv3lem2  6277  nnc3n3p1  6279  spacvallem1  6282  nchoicelem10  6299  nchoicelem11  6300  nchoicelem16  6305  dmfrec  6317  fnfreclem1  6318