Theorem exbidv 1874

Description: Formula-building rule for existential quantifier (deduction form). (Contributed by NM, 5-Aug-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-17 1575	. 2 |- ( ph -> A. x ph )
2		albidv.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	exbidh 1663	1 |- ( ph -> ( E. x ps <-> E. x ch ) )

Syntax hints:   -> wi 4   <-> wb 105   E.wex 1541

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11ev  1877  2exbidv  1917  3exbidv  1918  eubidh  2088  eubid  2089  eleq1w  2295  eleq2w  2296  eleq1  2297  eleq2  2298  rexbidv2  2547  ceqsex2  2857  alexeq  2946  ceqex  2947  sbc5  3069  sbcex2  3099  sbcexg  3100  sbcabel  3128  eluni  3922  csbunig  3927  intab  3983  cbvopab1  4188  cbvopab1s  4190  axsep2  4234  zfauscl  4235  bnd2  4291  mss  4347  opeqex  4371  euotd  4376  snnex  4574  uniuni  4577  regexmid  4662  reg2exmid  4663  onintexmid  4700  reg3exmid  4707  nnregexmid  4748  opeliunxp  4810  csbxpg  4836  brcog  4927  elrn2g  4950  dfdmf  4954  csbdmg  4955  eldmg  4956  dfrnf  5003  elrn2  5004  elrnmpt1  5013  brcodir  5155  xp11m  5206  xpimasn  5216  csbrng  5229  elxp4  5255  elxp5  5256  dfco2a  5268  cores  5271  funimaexglem  5444  brprcneu  5668  ssimaexg  5744  dmfco  5750  fndmdif  5788  fmptco  5848  fliftf  5978  acexmidlem2  6055  acexmidlemv  6056  cbvoprab1  6133  cbvoprab2  6134  oprssdmm  6378  dmtpos  6500  tfrlemi1  6576  tfr1onlemaccex  6592  tfrcllemaccex  6605  ecdmn0m  6824  ereldm  6825  elqsn0m  6850  mapsnd  6936  mapsn  6938  breng  6995  bren  6996  brdom2g  6997  brdomg  6998  domeng  7002  mapsnend  7065  en2  7078  ac6sfi  7168  ordiso  7340  ctssdclemr  7416  enumct  7419  ctssexmid  7454  sspw1or2  7508  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  acneq  7522  finacn  7524  acfun  7527  ccfunen  7594  cc1  7595  cc2lem  7596  cc2  7597  cc3  7598  acnccim  7602  recexnq  7721  prarloc  7834  genpdflem  7838  genpassl  7855  genpassu  7856  ltexprlemell  7929  ltexprlemelu  7930  ltexprlemm  7931  recexprlemell  7953  recexprlemelu  7954  cnm  8163  sup3exmid  9248  seq3f1olemp  10901  zfz1isolem1  11237  zfz1iso  11238  sumeq1  12065  sumeq2  12069  summodc  12094  fsum3  12098  fsum2dlemstep  12145  ntrivcvgap0  12260  prodeq1f  12263  prodeq2w  12267  prodeq2  12268  prodmodc  12289  zproddc  12290  fprodseq  12294  fprodntrivap  12295  fprod2dlemstep  12333  ctinf  13265  ctiunct  13275  ssomct  13280  ptex  13561  igsumvalx  13652  gsumpropd  13655  gsumpropd2  13656  gsumress  13658  gsum0g  13659  gfsumval  14102  islssm  14631  islssmg  14632  znleval  14927  uhgrm  16199  lpvtx  16200  incistruhgr  16211  upgrex  16224  uhgredgm  16257  subgruhgredgdm  16391  1loopgrvd2fi  16426  wlkm  16460  bdsep2  16782  bdzfauscl  16786  strcoll2  16879  sscoll2  16884  subctctexmid  16900  domomsubct  16901  nninfall  16913