Theorem exbidv 1836

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

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

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11ev  1839  2exbidv  1879  3exbidv  1880  eubidh  2048  eubid  2049  eleq1w  2254  eleq2w  2255  eleq1  2256  eleq2  2257  rexbidv2  2497  ceqsex2  2801  alexeq  2887  ceqex  2888  sbc5  3010  sbcex2  3040  sbcexg  3041  sbcabel  3068  eluni  3839  csbunig  3844  intab  3900  cbvopab1  4103  cbvopab1s  4105  axsep2  4149  zfauscl  4150  bnd2  4203  mss  4256  opeqex  4279  euotd  4284  snnex  4480  uniuni  4483  regexmid  4568  reg2exmid  4569  onintexmid  4606  reg3exmid  4613  nnregexmid  4654  opeliunxp  4715  csbxpg  4741  brcog  4830  elrn2g  4853  dfdmf  4856  csbdmg  4857  eldmg  4858  dfrnf  4904  elrn2  4905  elrnmpt1  4914  brcodir  5054  xp11m  5105  xpimasn  5115  csbrng  5128  elxp4  5154  elxp5  5155  dfco2a  5167  cores  5170  funimaexglem  5338  brprcneu  5548  ssimaexg  5620  dmfco  5626  fndmdif  5664  fmptco  5725  fliftf  5843  acexmidlem2  5916  acexmidlemv  5917  cbvoprab1  5991  cbvoprab2  5992  oprssdmm  6226  dmtpos  6311  tfrlemi1  6387  tfr1onlemaccex  6403  tfrcllemaccex  6416  ecdmn0m  6633  ereldm  6634  elqsn0m  6659  mapsn  6746  bren  6803  brdomg  6804  domeng  6808  ac6sfi  6956  ordiso  7097  ctssdclemr  7173  enumct  7176  ctssexmid  7211  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  acfun  7269  ccfunen  7326  cc1  7327  cc2lem  7328  cc2  7329  cc3  7330  recexnq  7452  prarloc  7565  genpdflem  7569  genpassl  7586  genpassu  7587  ltexprlemell  7660  ltexprlemelu  7661  ltexprlemm  7662  recexprlemell  7684  recexprlemelu  7685  cnm  7894  sup3exmid  8978  seq3f1olemp  10589  zfz1isolem1  10914  zfz1iso  10915  sumeq1  11501  sumeq2  11505  summodc  11529  fsum3  11533  fsum2dlemstep  11580  ntrivcvgap0  11695  prodeq1f  11698  prodeq2w  11702  prodeq2  11703  prodmodc  11724  zproddc  11725  fprodseq  11729  fprodntrivap  11730  fprod2dlemstep  11768  ctinf  12590  ctiunct  12600  ssomct  12605  ptex  12878  igsumvalx  12975  gsumpropd  12978  gsumpropd2  12979  gsumress  12981  gsum0g  12982  islssm  13856  islssmg  13857  znleval  14152  bdsep2  15448  bdzfauscl  15452  strcoll2  15545  sscoll2  15550  subctctexmid  15561  nninfall  15569