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  6531  tfrlemi1  6607  tfr1onlemaccex  6623  tfrcllemaccex  6636  ecdmn0m  6855  ereldm  6856  elqsn0m  6881  mapsnd  6974  mapsn  6976  breng  7033  bren  7034  brdom2g  7035  brdomg  7036  domeng  7040  mapsnend  7103  en2  7116  ac6sfi  7206  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  10973  zfz1isolem1  11314  zfz1iso  11315  sumeq1  12146  sumeq2  12150  summodc  12175  fsum3  12179  fsum2dlemstep  12226  ntrivcvgap0  12341  prodeq1f  12344  prodeq2w  12348  prodeq2  12349  prodmodc  12370  zproddc  12371  fprodseq  12375  fprodntrivap  12376  fprod2dlemstep  12414  ctinf  13379  ctiunct  13389  ssomct  13394  ptex  13677  gzsumvalx  13768  gzsumress  13771  gzsum0  13772  gsumvalfi  14242  islssm  14803  islssmg  14804  znleval  15097  uhgrm  16524  lpvtx  16525  incistruhgr  16536  upgrex  16549  uhgredgm  16582  subgruhgredgdm  16716  1loopgrvd2fi  16751  wlkm  16785  bdsep2  17117  bdsepg  17121  strcoll2  17214  sscoll2  17219  subctctexmid  17235  domomsubct  17236  wexmiddiffilem  17248  wexmiddifxylem  17250  nninfall  17258