Theorem exbidv 1873

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  1876  2exbidv  1916  3exbidv  1917  eubidh  2085  eubid  2086  eleq1w  2292  eleq2w  2293  eleq1  2294  eleq2  2295  rexbidv2  2536  ceqsex2  2845  alexeq  2933  ceqex  2934  sbc5  3056  sbcex2  3086  sbcexg  3087  sbcabel  3115  eluni  3901  csbunig  3906  intab  3962  cbvopab1  4167  cbvopab1s  4169  axsep2  4213  zfauscl  4214  bnd2  4269  mss  4324  opeqex  4348  euotd  4353  snnex  4551  uniuni  4554  regexmid  4639  reg2exmid  4640  onintexmid  4677  reg3exmid  4684  nnregexmid  4725  opeliunxp  4787  csbxpg  4813  brcog  4903  elrn2g  4926  dfdmf  4930  csbdmg  4931  eldmg  4932  dfrnf  4979  elrn2  4980  elrnmpt1  4989  brcodir  5131  xp11m  5182  xpimasn  5192  csbrng  5205  elxp4  5231  elxp5  5232  dfco2a  5244  cores  5247  funimaexglem  5420  brprcneu  5641  ssimaexg  5717  dmfco  5723  fndmdif  5761  fmptco  5821  fliftf  5950  acexmidlem2  6025  acexmidlemv  6026  cbvoprab1  6103  cbvoprab2  6104  oprssdmm  6343  dmtpos  6465  tfrlemi1  6541  tfr1onlemaccex  6557  tfrcllemaccex  6570  ecdmn0m  6789  ereldm  6790  elqsn0m  6815  mapsn  6902  breng  6959  bren  6960  brdom2g  6961  brdomg  6962  domeng  6966  en2  7041  ac6sfi  7130  ordiso  7295  ctssdclemr  7371  enumct  7374  ctssexmid  7409  sspw1or2  7463  exmidfodomrlemr  7473  exmidfodomrlemrALT  7474  acneq  7477  finacn  7479  acfun  7482  ccfunen  7543  cc1  7544  cc2lem  7545  cc2  7546  cc3  7547  acnccim  7551  recexnq  7670  prarloc  7783  genpdflem  7787  genpassl  7804  genpassu  7805  ltexprlemell  7878  ltexprlemelu  7879  ltexprlemm  7880  recexprlemell  7902  recexprlemelu  7903  cnm  8112  sup3exmid  9196  seq3f1olemp  10840  zfz1isolem1  11167  zfz1iso  11168  sumeq1  11995  sumeq2  11999  summodc  12024  fsum3  12028  fsum2dlemstep  12075  ntrivcvgap0  12190  prodeq1f  12193  prodeq2w  12197  prodeq2  12198  prodmodc  12219  zproddc  12220  fprodseq  12224  fprodntrivap  12225  fprod2dlemstep  12263  ctinf  13131  ctiunct  13141  ssomct  13146  ptex  13427  igsumvalx  13552  gsumpropd  13555  gsumpropd2  13556  gsumress  13558  gsum0g  13559  islssm  14453  islssmg  14454  znleval  14749  uhgrm  16019  lpvtx  16020  incistruhgr  16031  upgrex  16044  uhgredgm  16077  subgruhgredgdm  16211  1loopgrvd2fi  16246  wlkm  16280  bdsep2  16602  bdzfauscl  16606  strcoll2  16699  sscoll2  16704  subctctexmid  16722  domomsubct  16723  nninfall  16735  gfsumval  16809