Theorem exbidv 1849

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

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

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11ev  1852  2exbidv  1892  3exbidv  1893  eubidh  2061  eubid  2062  eleq1w  2268  eleq2w  2269  eleq1  2270  eleq2  2271  rexbidv2  2511  ceqsex2  2818  alexeq  2906  ceqex  2907  sbc5  3029  sbcex2  3059  sbcexg  3060  sbcabel  3088  eluni  3867  csbunig  3872  intab  3928  cbvopab1  4133  cbvopab1s  4135  axsep2  4179  zfauscl  4180  bnd2  4233  mss  4288  opeqex  4312  euotd  4317  snnex  4513  uniuni  4516  regexmid  4601  reg2exmid  4602  onintexmid  4639  reg3exmid  4646  nnregexmid  4687  opeliunxp  4748  csbxpg  4774  brcog  4863  elrn2g  4886  dfdmf  4890  csbdmg  4891  eldmg  4892  dfrnf  4938  elrn2  4939  elrnmpt1  4948  brcodir  5089  xp11m  5140  xpimasn  5150  csbrng  5163  elxp4  5189  elxp5  5190  dfco2a  5202  cores  5205  funimaexglem  5376  brprcneu  5592  ssimaexg  5664  dmfco  5670  fndmdif  5708  fmptco  5769  fliftf  5891  acexmidlem2  5964  acexmidlemv  5965  cbvoprab1  6040  cbvoprab2  6041  oprssdmm  6280  dmtpos  6365  tfrlemi1  6441  tfr1onlemaccex  6457  tfrcllemaccex  6470  ecdmn0m  6687  ereldm  6688  elqsn0m  6713  mapsn  6800  breng  6857  bren  6858  brdom2g  6859  brdomg  6860  domeng  6864  en2  6936  ac6sfi  7021  ordiso  7164  ctssdclemr  7240  enumct  7243  ctssexmid  7278  exmidfodomrlemr  7341  exmidfodomrlemrALT  7342  acneq  7345  finacn  7347  acfun  7350  ccfunen  7411  cc1  7412  cc2lem  7413  cc2  7414  cc3  7415  acnccim  7419  recexnq  7538  prarloc  7651  genpdflem  7655  genpassl  7672  genpassu  7673  ltexprlemell  7746  ltexprlemelu  7747  ltexprlemm  7748  recexprlemell  7770  recexprlemelu  7771  cnm  7980  sup3exmid  9065  seq3f1olemp  10697  zfz1isolem1  11022  zfz1iso  11023  sumeq1  11781  sumeq2  11785  summodc  11809  fsum3  11813  fsum2dlemstep  11860  ntrivcvgap0  11975  prodeq1f  11978  prodeq2w  11982  prodeq2  11983  prodmodc  12004  zproddc  12005  fprodseq  12009  fprodntrivap  12010  fprod2dlemstep  12048  ctinf  12916  ctiunct  12926  ssomct  12931  ptex  13211  igsumvalx  13336  gsumpropd  13339  gsumpropd2  13340  gsumress  13342  gsum0g  13343  islssm  14234  islssmg  14235  znleval  14530  uhgrm  15789  lpvtx  15790  incistruhgr  15801  upgrex  15814  uhgredgm  15842  bdsep2  16021  bdzfauscl  16025  strcoll2  16118  sscoll2  16123  subctctexmid  16139  domomsubct  16140  nninfall  16148