Theorem exbidv 1850

Description: Formula-building rule for existential quantifier (deduction rule). (Contributed by NM, 26-May-1993.)

Hypothesis

Ref	Expression
albidv.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
exbidv	|- ( ph -> ( E. x ps <-> E. x ch ) )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   ch( x)

Proof of Theorem exbidv

Step	Hyp	Ref	Expression
1		ax-5 1839	. 2 |- ( ph -> A. x ph )
2		albidv.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	exbidh 1794	1 |- ( ph -> ( E. x ps <-> E. x ch ) )

Syntax hints:   -> wi 4   <-> wb 196   E.wex 1704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-ex 1705

This theorem is referenced by:  2exbidv  1852  3exbidv  1853  eubid  2488  eleq1w  2684  eleq2w  2685  eleq1d  2686  eleq2dALT  2688  rexbidv2  3048  ceqsex2  3244  alexeqg  3332  sbc2or  3444  sbc5  3460  sbcex2  3486  sbcabel  3517  elpreqprlem  4395  elpreqpr  4396  eluni  4439  csbuni  4466  intab  4507  cbvopab1  4723  cbvopab1s  4725  axrep1  4772  axrep2  4773  axrep3  4774  zfrepclf  4777  axsep2  4782  zfauscl  4783  euotd  4975  opeliunxp  5170  brcog  5288  elrn2g  5313  dfdmf  5317  eldmg  5319  dfrnf  5364  elrn2  5365  elrnmpt1  5374  brcodir  5515  dfco2a  5635  cores  5638  sbcfung  5912  brprcneu  6184  ssimaexg  6264  dmfco  6272  fndmdif  6321  fmptco  6396  fliftf  6565  cbvoprab1  6727  cbvoprab2  6728  snnexOLD  6967  uniuni  6971  dmtpos  7364  wrecseq123  7408  wfrlem1  7414  wfrlem3a  7417  wfrlem15  7429  rdglim2  7528  ecdmn0  7789  mapsn  7899  bren  7964  brdomg  7965  domeng  7969  isinf  8173  ac6sfi  8204  ordiso  8421  brwdom  8472  brwdom2  8478  zfregcl  8499  zfregclOLD  8501  inf0  8518  zfinf  8536  bnd2  8756  isinffi  8818  acneq  8866  acni  8868  aceq0  8941  aceq3lem  8943  dfac3  8944  dfac5lem4  8949  dfac8  8957  dfac9  8958  kmlem1  8972  kmlem2  8973  kmlem8  8979  kmlem10  8981  kmlem13  8984  cfval  9069  cardcf  9074  cfeq0  9078  cfsuc  9079  cff1  9080  cflim3  9084  cofsmo  9091  isfin4  9119  axcc2lem  9258  axcc4dom  9263  domtriomlem  9264  dcomex  9269  axdc2lem  9270  axdc4lem  9277  zfac  9282  ac7g  9296  ac4c  9298  ac5  9299  ac6sg  9310  weth  9317  axrepndlem1  9414  axunndlem1  9417  zfcndrep  9436  zfcndinf  9440  zfcndac  9441  gruina  9640  grothomex  9651  genpass  9831  1idpr  9851  ltexprlem3  9860  ltexprlem4  9861  ltexpri  9865  reclem2pr  9870  reclem3pr  9871  recexpr  9873  infm3  10982  nnunb  11288  axdc4uz  12783  ishashinf  13247  relexpindlem  13803  sumeq1  14419  sumeq2w  14422  sumeq2ii  14423  summo  14448  fsum  14451  fsum2dlem  14501  ntrivcvgn0  14630  ntrivcvgmullem  14633  prodeq1f  14638  prodeq2w  14642  prodeq2ii  14643  prodmo  14666  zprod  14667  fprod  14671  fprodntriv  14672  fprod2dlem  14710  ncoprmgcdne1b  15363  vdwapun  15678  vdwmc  15682  vdwmc2  15683  isacs  16312  dfiso2  16432  brssc  16474  isssc  16480  equivestrcsetc  16792  dirge  17237  gsumvalx  17270  gsumpropd  17272  gsumpropd2lem  17273  gsumress  17276  gsumval3eu  18305  gsumval3lem2  18307  dprd2d2  18443  znleval  19903  neitr  20984  cmpcovf  21194  hausmapdom  21303  ptval  21373  elpt  21375  ptpjopn  21415  ptclsg  21418  ptcnp  21425  uffix2  21728  cnextf  21870  prdsxmslem2  22334  metustfbas  22362  metcld2  23105  dchrmusumlema  25182  dchrisum0lema  25203  istrkgld  25358  uvtxa01vtx0  26297  1loopgrvd2  26399  wspthsn  26735  iswspthn  26736  wspthsnon  26739  iswspthsnon  26741  wspthnon  26743  wlkiswwlks2  26761  wlkiswwlksupgr2  26763  wlklnwwlkln2lem  26768  wlksnwwlknvbij  26803  wspthsnwspthsnon  26811  elwwlks2on  26852  elwwlks2  26861  elwspths2spth  26862  clwlkclwwlk  26903  clwwlksvbij  26922  isgrpo  27351  adjeu  28748  fcoinvbr  29419  fmptcof2  29457  acunirnmpt  29459  acunirnmpt2  29460  acunirnmpt2f  29461  aciunf1  29463  fpwrelmapffslem  29507  fmcncfil  29977  bnj865  30993  bnj1388  31101  bnj1489  31124  eldm3  31651  opelco3  31678  frrlem1  31780  elsingles  32025  funpartlem  32049  dfrdg4  32058  linedegen  32250  finminlem  32312  filnetlem4  32376  bj-axrep1  32788  bj-axrep2  32789  bj-axrep3  32790  bj-issetwt  32859  bj-ax8  32887  bj-axsep2  32921  bj-restuni  33050  bj-finsumval0  33147  csbwrecsg  33173  csboprabg  33176  topdifinffinlem  33195  wl-sb8eut  33359  sdclem1  33539  fdc  33541  ismgmOLD  33649  isriscg  33783  eldm4  34037  exan3  34062  exanres  34063  eldmcnv  34113  islshpat  34304  lshpsmreu  34396  isopos  34467  islpln5  34821  islvol5  34865  pmapjat1  35139  dibelval3  36436  diblsmopel  36460  mapdpglem3  36964  hdmapglem7a  37219  dfac11  37632  clcnvlem  37930  dfhe3  38069  ntrneineine0lem  38381  iotasbc  38620  iotasbc2  38621  sbcexgOLD  38753  csbunigOLD  39051  csbxpgOLD  39053  csbrngOLD  39056  fnchoice  39188  mapsnd  39388  mapsnend  39391  axccdom  39416  axccd  39429  stoweidlem35  40252  stoweidlem39  40256  elsprel  41725  opeliun2xp  42111  bnd2d  42428