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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   E.wex 1545

This proof depends on 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 proof depends on definitions:  df-bi 117

This theorem is used 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  3938  csbunig  3943  intab  3999  cbvopab1  4205  cbvopab1s  4207  axsepg  4252  sepg  4253  zfausclOLD  4255  bnd2  4312  mss  4368  opeqex  4392  euotd  4397  snnex  4596  uniuni  4599  regexmid  4684  reg2exmid  4685  onintexmid  4722  reg3exmid  4729  nnregexmid  4770  opeliunxp  4832  csbxpg  4858  brcog  4949  elrn2g  4972  dfdmf  4976  csbdmg  4977  eldmg  4978  dfrnf  5025  elrn2  5026  elrnmpt1  5035  brcodir  5178  xp11m  5229  xpimasn  5239  csbrng  5252  elxp4  5278  elxp5  5279  dfco2a  5291  cores  5294  funimaexglem  5467  brprcneu  5691  ssimaexg  5768  dmfco  5776  fndmdif  5817  fmptco  5877  fliftf  6008  acexmidlem2  6085  acexmidlemv  6086  cbvoprab1  6163  cbvoprab2  6164  oprssdmm  6409  dmtpos  6532  tfrlemi1  6608  tfr1onlemaccex  6624  tfrcllemaccex  6637  ecdmn0m  6856  ereldm  6857  elqsn0m  6882  mapsnd  6976  mapsn  6978  breng  7035  bren  7036  brdom2g  7037  brdomg  7038  domeng  7042  mapsnend  7105  en2  7118  ac6sfi  7208  isfsuppfi  7296  ordiso  7382  ctssdclemr  7458  enumct  7461  ctssexmid  7496  sspw1or2  7550  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  acneq  7564  finacn  7566  acfun  7569  ccfunen  7636  cc1  7637  cc2lem  7638  cc2  7639  cc3  7640  acnccim  7644  recexnq  7763  prarloc  7876  genpdflem  7880  genpassl  7897  genpassu  7898  ltexprlemell  7971  ltexprlemelu  7972  ltexprlemm  7973  recexprlemell  7995  recexprlemelu  7996  cnm  8205  sup3exmid  9295  seq3f1olemp  10972  zfz1isolem1  11313  zfz1iso  11314  sumeq1  12145  sumeq2  12149  summodc  12174  fsum3  12178  fsum2dlemstep  12225  ntrivcvgap0  12340  prodeq1f  12343  prodeq2w  12347  prodeq2  12348  prodmodc  12369  zproddc  12370  fprodseq  12374  fprodntrivap  12375  fprod2dlemstep  12413  ctinf  13378  ctiunct  13388  ssomct  13393  ptex  13676  gzsumvalx  13767  gzsumress  13770  gzsum0  13771  gsumvalfi  14241  islssm  14802  islssmg  14803  znleval  15096  uhgrm  16541  lpvtx  16542  incistruhgr  16553  upgrex  16566  uhgredgm  16599  subgruhgredgdm  16733  1loopgrvd2fi  16768  wlkm  16802  bdsep2  17134  bdsepg  17138  strcoll2  17231  sscoll2  17236  subctctexmid  17252  domomsubct  17253  wexmiddiffilem  17265  wexmiddifxylem  17267  nninfall  17275