Theorem exbidv 1797

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

Syntax hints:   -> wi 4   <-> wb 104   E.wex 1468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ax11ev  1800  2exbidv  1840  3exbidv  1841  eubidh  2003  eubid  2004  eleq1w  2198  eleq2w  2199  eleq1  2200  eleq2  2201  rexbidv2  2438  ceqsex2  2721  alexeq  2806  ceqex  2807  sbc5  2927  sbcex2  2957  sbcexg  2958  sbcabel  2985  eluni  3734  csbunig  3739  intab  3795  cbvopab1  3996  cbvopab1s  3998  axsep2  4042  zfauscl  4043  bnd2  4092  mss  4143  opeqex  4166  euotd  4171  snnex  4364  uniuni  4367  regexmid  4445  reg2exmid  4446  onintexmid  4482  reg3exmid  4489  nnregexmid  4529  opeliunxp  4589  csbxpg  4615  brcog  4701  elrn2g  4724  dfdmf  4727  csbdmg  4728  eldmg  4729  dfrnf  4775  elrn2  4776  elrnmpt1  4785  brcodir  4921  xp11m  4972  xpimasn  4982  csbrng  4995  elxp4  5021  elxp5  5022  dfco2a  5034  cores  5037  funimaexglem  5201  brprcneu  5407  ssimaexg  5476  dmfco  5482  fndmdif  5518  fmptco  5579  fliftf  5693  acexmidlem2  5764  acexmidlemv  5765  cbvoprab1  5836  cbvoprab2  5837  oprssdmm  6062  dmtpos  6146  tfrlemi1  6222  tfr1onlemaccex  6238  tfrcllemaccex  6251  ecdmn0m  6464  ereldm  6465  elqsn0m  6490  mapsn  6577  bren  6634  brdomg  6635  domeng  6639  ac6sfi  6785  ordiso  6914  ctssdclemr  6990  enumct  6993  ctssexmid  7017  exmidfodomrlemr  7051  exmidfodomrlemrALT  7052  acfun  7056  ccfunen  7072  recexnq  7191  prarloc  7304  genpdflem  7308  genpassl  7325  genpassu  7326  ltexprlemell  7399  ltexprlemelu  7400  ltexprlemm  7401  recexprlemell  7423  recexprlemelu  7424  cnm  7633  sup3exmid  8708  seq3f1olemp  10268  zfz1isolem1  10576  zfz1iso  10577  sumeq1  11117  sumeq2  11121  summodc  11145  fsum3  11149  fsum2dlemstep  11196  ntrivcvgap0  11311  prodeq1f  11314  prodeq2w  11318  prodeq2  11319  ctinf  11932  ctiunct  11942  bdsep2  13073  bdzfauscl  13077  strcoll2  13170  subctctexmid  13185  nninfall  13193