Theorem exbidv 1848

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

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

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11ev  1851  2exbidv  1891  3exbidv  1892  eubidh  2060  eubid  2061  eleq1w  2266  eleq2w  2267  eleq1  2268  eleq2  2269  rexbidv2  2509  ceqsex2  2813  alexeq  2899  ceqex  2900  sbc5  3022  sbcex2  3052  sbcexg  3053  sbcabel  3080  eluni  3853  csbunig  3858  intab  3914  cbvopab1  4118  cbvopab1s  4120  axsep2  4164  zfauscl  4165  bnd2  4218  mss  4271  opeqex  4295  euotd  4300  snnex  4496  uniuni  4499  regexmid  4584  reg2exmid  4585  onintexmid  4622  reg3exmid  4629  nnregexmid  4670  opeliunxp  4731  csbxpg  4757  brcog  4846  elrn2g  4869  dfdmf  4872  csbdmg  4873  eldmg  4874  dfrnf  4920  elrn2  4921  elrnmpt1  4930  brcodir  5071  xp11m  5122  xpimasn  5132  csbrng  5145  elxp4  5171  elxp5  5172  dfco2a  5184  cores  5187  funimaexglem  5358  brprcneu  5571  ssimaexg  5643  dmfco  5649  fndmdif  5687  fmptco  5748  fliftf  5870  acexmidlem2  5943  acexmidlemv  5944  cbvoprab1  6019  cbvoprab2  6020  oprssdmm  6259  dmtpos  6344  tfrlemi1  6420  tfr1onlemaccex  6436  tfrcllemaccex  6449  ecdmn0m  6666  ereldm  6667  elqsn0m  6692  mapsn  6779  breng  6836  bren  6837  brdom2g  6838  brdomg  6839  domeng  6843  en2  6914  ac6sfi  6997  ordiso  7140  ctssdclemr  7216  enumct  7219  ctssexmid  7254  exmidfodomrlemr  7312  exmidfodomrlemrALT  7313  acneq  7316  finacn  7318  acfun  7321  ccfunen  7378  cc1  7379  cc2lem  7380  cc2  7381  cc3  7382  acnccim  7386  recexnq  7505  prarloc  7618  genpdflem  7622  genpassl  7639  genpassu  7640  ltexprlemell  7713  ltexprlemelu  7714  ltexprlemm  7715  recexprlemell  7737  recexprlemelu  7738  cnm  7947  sup3exmid  9032  seq3f1olemp  10662  zfz1isolem1  10987  zfz1iso  10988  sumeq1  11699  sumeq2  11703  summodc  11727  fsum3  11731  fsum2dlemstep  11778  ntrivcvgap0  11893  prodeq1f  11896  prodeq2w  11900  prodeq2  11901  prodmodc  11922  zproddc  11923  fprodseq  11927  fprodntrivap  11928  fprod2dlemstep  11966  ctinf  12834  ctiunct  12844  ssomct  12849  ptex  13129  igsumvalx  13254  gsumpropd  13257  gsumpropd2  13258  gsumress  13260  gsum0g  13261  islssm  14152  islssmg  14153  znleval  14448  bdsep2  15859  bdzfauscl  15863  strcoll2  15956  sscoll2  15961  subctctexmid  15974  domomsubct  15975  nninfall  15983