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

Theorem exbidv 1797
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
StepHypRef Expression
1 ax-17 1506 . 2 (𝜑 → ∀𝑥𝜑)
2 albidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2exbidh 1593 1 (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104  wex 1468
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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  ax11ev  1800  2exbidv  1840  3exbidv  1841  eubidh  2005  eubid  2006  eleq1w  2200  eleq2w  2201  eleq1  2202  eleq2  2203  rexbidv2  2440  ceqsex2  2726  alexeq  2811  ceqex  2812  sbc5  2932  sbcex2  2962  sbcexg  2963  sbcabel  2990  eluni  3739  csbunig  3744  intab  3800  cbvopab1  4001  cbvopab1s  4003  axsep2  4047  zfauscl  4048  bnd2  4097  mss  4148  opeqex  4171  euotd  4176  snnex  4369  uniuni  4372  regexmid  4450  reg2exmid  4451  onintexmid  4487  reg3exmid  4494  nnregexmid  4534  opeliunxp  4594  csbxpg  4620  brcog  4706  elrn2g  4729  dfdmf  4732  csbdmg  4733  eldmg  4734  dfrnf  4780  elrn2  4781  elrnmpt1  4790  brcodir  4926  xp11m  4977  xpimasn  4987  csbrng  5000  elxp4  5026  elxp5  5027  dfco2a  5039  cores  5042  funimaexglem  5206  brprcneu  5414  ssimaexg  5483  dmfco  5489  fndmdif  5525  fmptco  5586  fliftf  5700  acexmidlem2  5771  acexmidlemv  5772  cbvoprab1  5843  cbvoprab2  5844  oprssdmm  6069  dmtpos  6153  tfrlemi1  6229  tfr1onlemaccex  6245  tfrcllemaccex  6258  ecdmn0m  6471  ereldm  6472  elqsn0m  6497  mapsn  6584  bren  6641  brdomg  6642  domeng  6646  ac6sfi  6792  ordiso  6921  ctssdclemr  6997  enumct  7000  ctssexmid  7024  exmidfodomrlemr  7063  exmidfodomrlemrALT  7064  acfun  7068  ccfunen  7084  cc1  7085  cc2lem  7086  cc2  7087  cc3  7088  recexnq  7210  prarloc  7323  genpdflem  7327  genpassl  7344  genpassu  7345  ltexprlemell  7418  ltexprlemelu  7419  ltexprlemm  7420  recexprlemell  7442  recexprlemelu  7443  cnm  7652  sup3exmid  8727  seq3f1olemp  10287  zfz1isolem1  10595  zfz1iso  10596  sumeq1  11136  sumeq2  11140  summodc  11164  fsum3  11168  fsum2dlemstep  11215  ntrivcvgap0  11330  prodeq1f  11333  prodeq2w  11337  prodeq2  11338  prodmodc  11359  ctinf  11954  ctiunct  11964  bdsep2  13143  bdzfauscl  13147  strcoll2  13240  subctctexmid  13255  nninfall  13265
  Copyright terms: Public domain W3C validator