Theorem exbidv 1798

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 1507	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		albidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	exbidh 1594	1 ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 104  ∃wex 1469

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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ax11ev  1801  2exbidv  1841  3exbidv  1842  eubidh  2006  eubid  2007  eleq1w  2201  eleq2w  2202  eleq1  2203  eleq2  2204  rexbidv2  2441  ceqsex2  2729  alexeq  2815  ceqex  2816  sbc5  2936  sbcex2  2966  sbcexg  2967  sbcabel  2994  eluni  3747  csbunig  3752  intab  3808  cbvopab1  4009  cbvopab1s  4011  axsep2  4055  zfauscl  4056  bnd2  4105  mss  4156  opeqex  4179  euotd  4184  snnex  4377  uniuni  4380  regexmid  4458  reg2exmid  4459  onintexmid  4495  reg3exmid  4502  nnregexmid  4542  opeliunxp  4602  csbxpg  4628  brcog  4714  elrn2g  4737  dfdmf  4740  csbdmg  4741  eldmg  4742  dfrnf  4788  elrn2  4789  elrnmpt1  4798  brcodir  4934  xp11m  4985  xpimasn  4995  csbrng  5008  elxp4  5034  elxp5  5035  dfco2a  5047  cores  5050  funimaexglem  5214  brprcneu  5422  ssimaexg  5491  dmfco  5497  fndmdif  5533  fmptco  5594  fliftf  5708  acexmidlem2  5779  acexmidlemv  5780  cbvoprab1  5851  cbvoprab2  5852  oprssdmm  6077  dmtpos  6161  tfrlemi1  6237  tfr1onlemaccex  6253  tfrcllemaccex  6266  ecdmn0m  6479  ereldm  6480  elqsn0m  6505  mapsn  6592  bren  6649  brdomg  6650  domeng  6654  ac6sfi  6800  ordiso  6929  ctssdclemr  7005  enumct  7008  ctssexmid  7032  exmidfodomrlemr  7075  exmidfodomrlemrALT  7076  acfun  7080  ccfunen  7096  cc1  7097  cc2lem  7098  cc2  7099  cc3  7100  recexnq  7222  prarloc  7335  genpdflem  7339  genpassl  7356  genpassu  7357  ltexprlemell  7430  ltexprlemelu  7431  ltexprlemm  7432  recexprlemell  7454  recexprlemelu  7455  cnm  7664  sup3exmid  8739  seq3f1olemp  10306  zfz1isolem1  10615  zfz1iso  10616  sumeq1  11156  sumeq2  11160  summodc  11184  fsum3  11188  fsum2dlemstep  11235  ntrivcvgap0  11350  prodeq1f  11353  prodeq2w  11357  prodeq2  11358  prodmodc  11379  zproddc  11380  fprodseq  11384  ctinf  11979  ctiunct  11989  bdsep2  13255  bdzfauscl  13259  strcoll2  13352  sscoll2  13357  subctctexmid  13369  nninfall  13379