Theorem exbidv 1873

Description: Formula-building rule for existential quantifier (deduction form). (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
albidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
exbidv	⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem exbidv

Step	Hyp	Ref	Expression
1		ax-17 1574	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		albidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	exbidh 1662	1 ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 105  ∃wex 1540

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582

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  2535  ceqsex2  2844  alexeq  2932  ceqex  2933  sbc5  3055  sbcex2  3085  sbcexg  3086  sbcabel  3114  eluni  3896  csbunig  3901  intab  3957  cbvopab1  4162  cbvopab1s  4164  axsep2  4208  zfauscl  4209  bnd2  4263  mss  4318  opeqex  4342  euotd  4347  snnex  4545  uniuni  4548  regexmid  4633  reg2exmid  4634  onintexmid  4671  reg3exmid  4678  nnregexmid  4719  opeliunxp  4781  csbxpg  4807  brcog  4897  elrn2g  4920  dfdmf  4924  csbdmg  4925  eldmg  4926  dfrnf  4973  elrn2  4974  elrnmpt1  4983  brcodir  5124  xp11m  5175  xpimasn  5185  csbrng  5198  elxp4  5224  elxp5  5225  dfco2a  5237  cores  5240  funimaexglem  5413  brprcneu  5632  ssimaexg  5708  dmfco  5714  fndmdif  5752  fmptco  5813  fliftf  5940  acexmidlem2  6015  acexmidlemv  6016  cbvoprab1  6093  cbvoprab2  6094  oprssdmm  6334  dmtpos  6422  tfrlemi1  6498  tfr1onlemaccex  6514  tfrcllemaccex  6527  ecdmn0m  6746  ereldm  6747  elqsn0m  6772  mapsn  6859  breng  6916  bren  6917  brdom2g  6918  brdomg  6919  domeng  6923  en2  6998  ac6sfi  7087  ordiso  7235  ctssdclemr  7311  enumct  7314  ctssexmid  7349  sspw1or2  7403  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  acneq  7417  finacn  7419  acfun  7422  ccfunen  7483  cc1  7484  cc2lem  7485  cc2  7486  cc3  7487  acnccim  7491  recexnq  7610  prarloc  7723  genpdflem  7727  genpassl  7744  genpassu  7745  ltexprlemell  7818  ltexprlemelu  7819  ltexprlemm  7820  recexprlemell  7842  recexprlemelu  7843  cnm  8052  sup3exmid  9137  seq3f1olemp  10778  zfz1isolem1  11105  zfz1iso  11106  sumeq1  11933  sumeq2  11937  summodc  11962  fsum3  11966  fsum2dlemstep  12013  ntrivcvgap0  12128  prodeq1f  12131  prodeq2w  12135  prodeq2  12136  prodmodc  12157  zproddc  12158  fprodseq  12162  fprodntrivap  12163  fprod2dlemstep  12201  ctinf  13069  ctiunct  13079  ssomct  13084  ptex  13365  igsumvalx  13490  gsumpropd  13493  gsumpropd2  13494  gsumress  13496  gsum0g  13497  islssm  14390  islssmg  14391  znleval  14686  uhgrm  15948  lpvtx  15949  incistruhgr  15960  upgrex  15973  uhgredgm  16006  subgruhgredgdm  16140  1loopgrvd2fi  16175  wlkm  16209  bdsep2  16532  bdzfauscl  16536  strcoll2  16629  sscoll2  16634  subctctexmid  16652  domomsubct  16653  nninfall  16662  gfsumval  16732