Theorem exbidv 1874

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

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

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11ev  1877  2exbidv  1917  3exbidv  1918  eubidh  2088  eubid  2089  eleq1w  2295  eleq2w  2296  eleq1  2297  eleq2  2298  rexbidv2  2547  ceqsex2  2857  alexeq  2945  ceqex  2946  sbc5  3068  sbcex2  3098  sbcexg  3099  sbcabel  3127  eluni  3919  csbunig  3924  intab  3980  cbvopab1  4185  cbvopab1s  4187  axsep2  4231  zfauscl  4232  bnd2  4288  mss  4344  opeqex  4368  euotd  4373  snnex  4571  uniuni  4574  regexmid  4659  reg2exmid  4660  onintexmid  4697  reg3exmid  4704  nnregexmid  4745  opeliunxp  4807  csbxpg  4833  brcog  4924  elrn2g  4947  dfdmf  4951  csbdmg  4952  eldmg  4953  dfrnf  5000  elrn2  5001  elrnmpt1  5010  brcodir  5152  xp11m  5203  xpimasn  5213  csbrng  5226  elxp4  5252  elxp5  5253  dfco2a  5265  cores  5268  funimaexglem  5441  brprcneu  5665  ssimaexg  5741  dmfco  5747  fndmdif  5785  fmptco  5845  fliftf  5974  acexmidlem2  6049  acexmidlemv  6050  cbvoprab1  6127  cbvoprab2  6128  oprssdmm  6367  dmtpos  6489  tfrlemi1  6565  tfr1onlemaccex  6581  tfrcllemaccex  6594  ecdmn0m  6813  ereldm  6814  elqsn0m  6839  mapsnd  6925  mapsn  6927  breng  6984  bren  6985  brdom2g  6986  brdomg  6987  domeng  6991  mapsnend  7054  en2  7067  ac6sfi  7157  ordiso  7329  ctssdclemr  7405  enumct  7408  ctssexmid  7443  sspw1or2  7497  exmidfodomrlemr  7507  exmidfodomrlemrALT  7508  acneq  7511  finacn  7513  acfun  7516  ccfunen  7580  cc1  7581  cc2lem  7582  cc2  7583  cc3  7584  acnccim  7588  recexnq  7707  prarloc  7820  genpdflem  7824  genpassl  7841  genpassu  7842  ltexprlemell  7915  ltexprlemelu  7916  ltexprlemm  7917  recexprlemell  7939  recexprlemelu  7940  cnm  8149  sup3exmid  9233  seq3f1olemp  10881  zfz1isolem1  11216  zfz1iso  11217  sumeq1  12044  sumeq2  12048  summodc  12073  fsum3  12077  fsum2dlemstep  12124  ntrivcvgap0  12239  prodeq1f  12242  prodeq2w  12246  prodeq2  12247  prodmodc  12268  zproddc  12269  fprodseq  12273  fprodntrivap  12274  fprod2dlemstep  12312  ctinf  13198  ctiunct  13208  ssomct  13213  ptex  13494  igsumvalx  13619  gsumpropd  13622  gsumpropd2  13623  gsumress  13625  gsum0g  13626  islssm  14522  islssmg  14523  znleval  14818  uhgrm  16090  lpvtx  16091  incistruhgr  16102  upgrex  16115  uhgredgm  16148  subgruhgredgdm  16282  1loopgrvd2fi  16317  wlkm  16351  bdsep2  16673  bdzfauscl  16677  strcoll2  16770  sscoll2  16775  subctctexmid  16791  domomsubct  16792  nninfall  16804  gfsumval  16879