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  5622  ssimaexg  5698  dmfco  5704  fndmdif  5742  fmptco  5803  fliftf  5929  acexmidlem2  6004  acexmidlemv  6005  cbvoprab1  6082  cbvoprab2  6083  oprssdmm  6323  dmtpos  6408  tfrlemi1  6484  tfr1onlemaccex  6500  tfrcllemaccex  6513  ecdmn0m  6732  ereldm  6733  elqsn0m  6758  mapsn  6845  breng  6902  bren  6903  brdom2g  6904  brdomg  6905  domeng  6909  en2  6981  ac6sfi  7068  ordiso  7214  ctssdclemr  7290  enumct  7293  ctssexmid  7328  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  acneq  7395  finacn  7397  acfun  7400  ccfunen  7461  cc1  7462  cc2lem  7463  cc2  7464  cc3  7465  acnccim  7469  recexnq  7588  prarloc  7701  genpdflem  7705  genpassl  7722  genpassu  7723  ltexprlemell  7796  ltexprlemelu  7797  ltexprlemm  7798  recexprlemell  7820  recexprlemelu  7821  cnm  8030  sup3exmid  9115  seq3f1olemp  10749  zfz1isolem1  11075  zfz1iso  11076  sumeq1  11882  sumeq2  11886  summodc  11910  fsum3  11914  fsum2dlemstep  11961  ntrivcvgap0  12076  prodeq1f  12079  prodeq2w  12083  prodeq2  12084  prodmodc  12105  zproddc  12106  fprodseq  12110  fprodntrivap  12111  fprod2dlemstep  12149  ctinf  13017  ctiunct  13027  ssomct  13032  ptex  13313  igsumvalx  13438  gsumpropd  13441  gsumpropd2  13442  gsumress  13444  gsum0g  13445  islssm  14337  islssmg  14338  znleval  14633  uhgrm  15894  lpvtx  15895  incistruhgr  15906  upgrex  15919  uhgredgm  15950  wlkm  16085  bdsep2  16332  bdzfauscl  16336  strcoll2  16429  sscoll2  16434  subctctexmid  16453  domomsubct  16454  nninfall  16463