ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  exbidv GIF version

Theorem exbidv 1706
Description: Formula-building rule for existential quantifier (deduction rule). (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
StepHypRef Expression
1 ax-17 1419 . 2 (𝜑 → ∀𝑥𝜑)
2 albidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2exbidh 1505 1 (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98  wex 1381
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  ax11ev  1709  2exbidv  1748  3exbidv  1749  eubidh  1906  eubid  1907  eleq1  2100  eleq2  2101  rexbidv2  2326  ceqsex2  2591  alexeq  2667  ceqex  2668  sbc5  2784  sbcex2  2809  sbcexg  2810  sbcabel  2836  eluni  3580  csbunig  3585  intab  3641  cbvopab1  3827  cbvopab1s  3829  axsep2  3873  zfauscl  3874  bnd2  3923  mss  3959  opeqex  3983  euotd  3988  snnex  4177  uniuni  4179  regexmid  4255  nnregexmid  4329  opeliunxp  4382  csbxpg  4408  brcog  4489  elrn2g  4512  dfdmf  4515  csbdmg  4516  eldmg  4517  dfrnf  4562  elrn2  4563  elrnmpt1  4572  brcodir  4699  xp11m  4746  xpimasn  4756  csbrng  4769  elxp4  4795  elxp5  4796  dfco2a  4808  cores  4811  funimaexglem  4969  brprcneu  5158  ssimaexg  5222  dmfco  5228  fndmdif  5259  fmptco  5317  fliftf  5426  acexmidlem2  5496  acexmidlemv  5497  cbvoprab1  5563  cbvoprab2  5564  dmtpos  5858  tfrlemi1  5933  ecdmn0m  6135  ereldm  6136  elqsn0m  6161  bren  6215  brdomg  6216  domeng  6220  ac6sfi  6338  recexnq  6469  prarloc  6582  genpdflem  6586  genpassl  6603  genpassu  6604  ltexprlemell  6677  ltexprlemelu  6678  ltexprlemm  6679  recexprlemell  6701  recexprlemelu  6702  sumeq1  9751  bdsep2  9879  bdzfauscl  9883  strcoll2  9981
  Copyright terms: Public domain W3C validator