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  4117  cbvopab1s  4119  axsep2  4163  zfauscl  4164  bnd2  4217  mss  4270  opeqex  4294  euotd  4299  snnex  4495  uniuni  4498  regexmid  4583  reg2exmid  4584  onintexmid  4621  reg3exmid  4628  nnregexmid  4669  opeliunxp  4730  csbxpg  4756  brcog  4845  elrn2g  4868  dfdmf  4871  csbdmg  4872  eldmg  4873  dfrnf  4919  elrn2  4920  elrnmpt1  4929  brcodir  5070  xp11m  5121  xpimasn  5131  csbrng  5144  elxp4  5170  elxp5  5171  dfco2a  5183  cores  5186  funimaexglem  5357  brprcneu  5569  ssimaexg  5641  dmfco  5647  fndmdif  5685  fmptco  5746  fliftf  5868  acexmidlem2  5941  acexmidlemv  5942  cbvoprab1  6017  cbvoprab2  6018  oprssdmm  6257  dmtpos  6342  tfrlemi1  6418  tfr1onlemaccex  6434  tfrcllemaccex  6447  ecdmn0m  6664  ereldm  6665  elqsn0m  6690  mapsn  6777  breng  6834  bren  6835  brdom2g  6836  brdomg  6837  domeng  6841  en2  6912  ac6sfi  6995  ordiso  7138  ctssdclemr  7214  enumct  7217  ctssexmid  7252  exmidfodomrlemr  7310  exmidfodomrlemrALT  7311  acneq  7314  finacn  7316  acfun  7319  ccfunen  7376  cc1  7377  cc2lem  7378  cc2  7379  cc3  7380  acnccim  7384  recexnq  7503  prarloc  7616  genpdflem  7620  genpassl  7637  genpassu  7638  ltexprlemell  7711  ltexprlemelu  7712  ltexprlemm  7713  recexprlemell  7735  recexprlemelu  7736  cnm  7945  sup3exmid  9030  seq3f1olemp  10660  zfz1isolem1  10985  zfz1iso  10986  sumeq1  11666  sumeq2  11670  summodc  11694  fsum3  11698  fsum2dlemstep  11745  ntrivcvgap0  11860  prodeq1f  11863  prodeq2w  11867  prodeq2  11868  prodmodc  11889  zproddc  11890  fprodseq  11894  fprodntrivap  11895  fprod2dlemstep  11933  ctinf  12801  ctiunct  12811  ssomct  12816  ptex  13096  igsumvalx  13221  gsumpropd  13224  gsumpropd2  13225  gsumress  13227  gsum0g  13228  islssm  14119  islssmg  14120  znleval  14415  bdsep2  15826  bdzfauscl  15830  strcoll2  15923  sscoll2  15928  subctctexmid  15941  domomsubct  15942  nninfall  15950