Theorem exbidv 1878

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

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

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11ev  1881  2exbidv  1921  3exbidv  1922  eubidh  2092  eubid  2093  eleq1w  2299  eleq2w  2300  eleq1  2301  eleq2  2302  rexbidv2  2553  ceqsex2  2863  alexeq  2952  ceqex  2953  sbc5  3075  sbcex2  3105  sbcexg  3106  sbcabel  3134  eluni  3933  csbunig  3938  intab  3994  cbvopab1  4199  cbvopab1s  4201  axsepg  4245  sepg  4246  zfausclOLD  4248  bnd2  4305  mss  4361  opeqex  4385  euotd  4390  snnex  4589  uniuni  4592  regexmid  4677  reg2exmid  4678  onintexmid  4715  reg3exmid  4722  nnregexmid  4763  opeliunxp  4825  csbxpg  4851  brcog  4942  elrn2g  4965  dfdmf  4969  csbdmg  4970  eldmg  4971  dfrnf  5018  elrn2  5019  elrnmpt1  5028  brcodir  5170  xp11m  5221  xpimasn  5231  csbrng  5244  elxp4  5270  elxp5  5271  dfco2a  5283  cores  5286  funimaexglem  5459  brprcneu  5683  ssimaexg  5759  dmfco  5767  fndmdif  5805  fmptco  5865  fliftf  5995  acexmidlem2  6072  acexmidlemv  6073  cbvoprab1  6150  cbvoprab2  6151  oprssdmm  6395  dmtpos  6517  tfrlemi1  6593  tfr1onlemaccex  6609  tfrcllemaccex  6622  ecdmn0m  6841  ereldm  6842  elqsn0m  6867  mapsnd  6960  mapsn  6962  breng  7019  bren  7020  brdom2g  7021  brdomg  7022  domeng  7026  mapsnend  7089  en2  7102  ac6sfi  7192  ordiso  7366  ctssdclemr  7442  enumct  7445  ctssexmid  7480  sspw1or2  7534  exmidfodomrlemr  7544  exmidfodomrlemrALT  7545  acneq  7548  finacn  7550  acfun  7553  ccfunen  7620  cc1  7621  cc2lem  7622  cc2  7623  cc3  7624  acnccim  7628  recexnq  7747  prarloc  7860  genpdflem  7864  genpassl  7881  genpassu  7882  ltexprlemell  7955  ltexprlemelu  7956  ltexprlemm  7957  recexprlemell  7979  recexprlemelu  7980  cnm  8189  sup3exmid  9277  seq3f1olemp  10930  zfz1isolem1  11270  zfz1iso  11271  sumeq1  12099  sumeq2  12103  summodc  12128  fsum3  12132  fsum2dlemstep  12179  ntrivcvgap0  12294  prodeq1f  12297  prodeq2w  12301  prodeq2  12302  prodmodc  12323  zproddc  12324  fprodseq  12328  fprodntrivap  12329  fprod2dlemstep  12367  ctinf  13299  ctiunct  13309  ssomct  13314  ptex  13595  gzsumvalx  13686  gzsumress  13689  gzsum0  13690  gsumvalfi  14129  islssm  14666  islssmg  14667  znleval  14960  uhgrm  16233  lpvtx  16234  incistruhgr  16245  upgrex  16258  uhgredgm  16291  subgruhgredgdm  16425  1loopgrvd2fi  16460  wlkm  16494  bdsep2  16826  bdsepg  16830  strcoll2  16923  sscoll2  16928  subctctexmid  16944  domomsubct  16945  nninfall  16957