ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ralbidv Structured version   Unicode version

Theorem ralbidv 2320
Description: Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 20-Nov-1994.)
Hypothesis
Ref Expression
ralbidv.1
Assertion
Ref Expression
ralbidv
Distinct variable group:   ,
Allowed substitution hints:   ()   ()   ()

Proof of Theorem ralbidv
StepHypRef Expression
1 nfv 1418 . 2  F/
2 ralbidv.1 . 2
31, 2ralbid 2318 1
Colors of variables: wff set class
Syntax hints:   wi 4   wb 98  wral 2300
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 1333  ax-gen 1335  ax-4 1397  ax-17 1416
This theorem depends on definitions:  df-bi 110  df-nf 1347  df-ral 2305
This theorem is referenced by:  ralbii  2324  2ralbidv  2342  rexralbidv  2344  r19.32vdc  2453  raleqbi1dv  2507  raleqbidv  2511  cbvral2v  2535  rspc2  2655  rspc3v  2659  reu6i  2726  reu7  2730  sbcralt  2828  sbcralg  2830  raaanlem  3320  r19.12sn  3427  2ralunsn  3560  elintg  3614  elintrabg  3619  eliin  3653  bnd2  3917  poeq1  4027  soeq1  4043  reusv3  4158  posng  4355  ralxpf  4425  cnvpom  4803  funcnvuni  4911  dff4im  5256  dff13f  5352  eusvobj2  5441  ofreq  5657  smoeq  5846  recseq  5862  tfr0  5878  tfrlemiex  5886  elinp  6456  prloc  6473  nnsub  7693  indstr  8272  ublbneg  8284  lbzbi  8287  iccsupr  8565  bj-omtrans  9344
  Copyright terms: Public domain W3C validator