Theorem exbidv 1871

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

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

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11ev  1874  2exbidv  1914  3exbidv  1915  eubidh  2083  eubid  2084  eleq1w  2290  eleq2w  2291  eleq1  2292  eleq2  2293  rexbidv2  2533  ceqsex2  2841  alexeq  2929  ceqex  2930  sbc5  3052  sbcex2  3082  sbcexg  3083  sbcabel  3111  eluni  3891  csbunig  3896  intab  3952  cbvopab1  4157  cbvopab1s  4159  axsep2  4203  zfauscl  4204  bnd2  4257  mss  4312  opeqex  4336  euotd  4341  snnex  4539  uniuni  4542  regexmid  4627  reg2exmid  4628  onintexmid  4665  reg3exmid  4672  nnregexmid  4713  opeliunxp  4774  csbxpg  4800  brcog  4889  elrn2g  4912  dfdmf  4916  csbdmg  4917  eldmg  4918  dfrnf  4965  elrn2  4966  elrnmpt1  4975  brcodir  5116  xp11m  5167  xpimasn  5177  csbrng  5190  elxp4  5216  elxp5  5217  dfco2a  5229  cores  5232  funimaexglem  5404  brprcneu  5620  ssimaexg  5696  dmfco  5702  fndmdif  5740  fmptco  5801  fliftf  5923  acexmidlem2  5998  acexmidlemv  5999  cbvoprab1  6076  cbvoprab2  6077  oprssdmm  6317  dmtpos  6402  tfrlemi1  6478  tfr1onlemaccex  6494  tfrcllemaccex  6507  ecdmn0m  6724  ereldm  6725  elqsn0m  6750  mapsn  6837  breng  6894  bren  6895  brdom2g  6896  brdomg  6897  domeng  6901  en2  6973  ac6sfi  7060  ordiso  7203  ctssdclemr  7279  enumct  7282  ctssexmid  7317  exmidfodomrlemr  7380  exmidfodomrlemrALT  7381  acneq  7384  finacn  7386  acfun  7389  ccfunen  7450  cc1  7451  cc2lem  7452  cc2  7453  cc3  7454  acnccim  7458  recexnq  7577  prarloc  7690  genpdflem  7694  genpassl  7711  genpassu  7712  ltexprlemell  7785  ltexprlemelu  7786  ltexprlemm  7787  recexprlemell  7809  recexprlemelu  7810  cnm  8019  sup3exmid  9104  seq3f1olemp  10737  zfz1isolem1  11062  zfz1iso  11063  sumeq1  11866  sumeq2  11870  summodc  11894  fsum3  11898  fsum2dlemstep  11945  ntrivcvgap0  12060  prodeq1f  12063  prodeq2w  12067  prodeq2  12068  prodmodc  12089  zproddc  12090  fprodseq  12094  fprodntrivap  12095  fprod2dlemstep  12133  ctinf  13001  ctiunct  13011  ssomct  13016  ptex  13297  igsumvalx  13422  gsumpropd  13425  gsumpropd2  13426  gsumress  13428  gsum0g  13429  islssm  14321  islssmg  14322  znleval  14617  uhgrm  15878  lpvtx  15879  incistruhgr  15890  upgrex  15903  uhgredgm  15934  wlkm  16051  bdsep2  16249  bdzfauscl  16253  strcoll2  16346  sscoll2  16351  subctctexmid  16366  domomsubct  16367  nninfall  16375