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

Theorem exbidv 1750
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 1462 . 2 (𝜑 → ∀𝑥𝜑)
2 albidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2exbidh 1548 1 (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103  wex 1424
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-4 1443  ax-17 1462  ax-ial 1470
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  ax11ev  1753  2exbidv  1793  3exbidv  1794  eubidh  1951  eubid  1952  eleq1w  2145  eleq2w  2146  eleq1  2147  eleq2  2148  rexbidv2  2379  ceqsex2  2653  alexeq  2734  ceqex  2735  sbc5  2852  sbcex2  2881  sbcexg  2882  sbcabel  2909  eluni  3641  csbunig  3646  intab  3702  cbvopab1  3888  cbvopab1s  3890  axsep2  3935  zfauscl  3936  bnd2  3985  mss  4029  opeqex  4052  euotd  4057  snnex  4247  uniuni  4249  regexmid  4326  reg2exmid  4327  onintexmid  4363  reg3exmid  4370  nnregexmid  4409  opeliunxp  4463  csbxpg  4489  brcog  4573  elrn2g  4596  dfdmf  4599  csbdmg  4600  eldmg  4601  dfrnf  4646  elrn2  4647  elrnmpt1  4656  brcodir  4788  xp11m  4837  xpimasn  4847  csbrng  4860  elxp4  4886  elxp5  4887  dfco2a  4899  cores  4902  funimaexglem  5064  brprcneu  5263  ssimaexg  5331  dmfco  5337  fndmdif  5369  fmptco  5429  fliftf  5541  acexmidlem2  5612  acexmidlemv  5613  cbvoprab1  5679  cbvoprab2  5680  dmtpos  5977  tfrlemi1  6053  tfr1onlemaccex  6069  tfrcllemaccex  6082  ecdmn0m  6288  ereldm  6289  elqsn0m  6314  mapsn  6401  bren  6418  brdomg  6419  domeng  6423  ac6sfi  6568  ordiso  6676  exmidfodomrlemr  6775  exmidfodomrlemrALT  6776  recexnq  6896  prarloc  7009  genpdflem  7013  genpassl  7030  genpassu  7031  ltexprlemell  7104  ltexprlemelu  7105  ltexprlemm  7106  recexprlemell  7128  recexprlemelu  7129  iseqf1olemp  9839  zfz1isolem1  10145  zfz1iso  10146  sumeq1  10639  sumeq2  10643  isummo  10667  fisum  10670  bdsep2  11246  bdzfauscl  11250  strcoll2  11347  nninfall  11369
  Copyright terms: Public domain W3C validator