Theorem exbidv 1873

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 1574	. 2 |- ( ph -> A. x ph )
2		albidv.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	exbidh 1662	1 |- ( ph -> ( E. x ps <-> E. x ch ) )

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

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11ev  1876  2exbidv  1916  3exbidv  1917  eubidh  2085  eubid  2086  eleq1w  2292  eleq2w  2293  eleq1  2294  eleq2  2295  rexbidv2  2535  ceqsex2  2844  alexeq  2932  ceqex  2933  sbc5  3055  sbcex2  3085  sbcexg  3086  sbcabel  3114  eluni  3896  csbunig  3901  intab  3957  cbvopab1  4162  cbvopab1s  4164  axsep2  4208  zfauscl  4209  bnd2  4263  mss  4318  opeqex  4342  euotd  4347  snnex  4545  uniuni  4548  regexmid  4633  reg2exmid  4634  onintexmid  4671  reg3exmid  4678  nnregexmid  4719  opeliunxp  4781  csbxpg  4807  brcog  4897  elrn2g  4920  dfdmf  4924  csbdmg  4925  eldmg  4926  dfrnf  4973  elrn2  4974  elrnmpt1  4983  brcodir  5124  xp11m  5175  xpimasn  5185  csbrng  5198  elxp4  5224  elxp5  5225  dfco2a  5237  cores  5240  funimaexglem  5413  brprcneu  5632  ssimaexg  5708  dmfco  5714  fndmdif  5752  fmptco  5813  fliftf  5939  acexmidlem2  6014  acexmidlemv  6015  cbvoprab1  6092  cbvoprab2  6093  oprssdmm  6333  dmtpos  6421  tfrlemi1  6497  tfr1onlemaccex  6513  tfrcllemaccex  6526  ecdmn0m  6745  ereldm  6746  elqsn0m  6771  mapsn  6858  breng  6915  bren  6916  brdom2g  6917  brdomg  6918  domeng  6922  en2  6997  ac6sfi  7086  ordiso  7234  ctssdclemr  7310  enumct  7313  ctssexmid  7348  sspw1or2  7402  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  acneq  7416  finacn  7418  acfun  7421  ccfunen  7482  cc1  7483  cc2lem  7484  cc2  7485  cc3  7486  acnccim  7490  recexnq  7609  prarloc  7722  genpdflem  7726  genpassl  7743  genpassu  7744  ltexprlemell  7817  ltexprlemelu  7818  ltexprlemm  7819  recexprlemell  7841  recexprlemelu  7842  cnm  8051  sup3exmid  9136  seq3f1olemp  10776  zfz1isolem1  11103  zfz1iso  11104  sumeq1  11915  sumeq2  11919  summodc  11943  fsum3  11947  fsum2dlemstep  11994  ntrivcvgap0  12109  prodeq1f  12112  prodeq2w  12116  prodeq2  12117  prodmodc  12138  zproddc  12139  fprodseq  12143  fprodntrivap  12144  fprod2dlemstep  12182  ctinf  13050  ctiunct  13060  ssomct  13065  ptex  13346  igsumvalx  13471  gsumpropd  13474  gsumpropd2  13475  gsumress  13477  gsum0g  13478  islssm  14370  islssmg  14371  znleval  14666  uhgrm  15928  lpvtx  15929  incistruhgr  15940  upgrex  15953  uhgredgm  15986  subgruhgredgdm  16120  1loopgrvd2fi  16155  wlkm  16189  bdsep2  16481  bdzfauscl  16485  strcoll2  16578  sscoll2  16583  subctctexmid  16601  domomsubct  16602  nninfall  16611  gfsumval  16680