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

Theorem rgen 2368
Description: Generalization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)
Hypothesis
Ref Expression
rgen.1
Assertion
Ref Expression
rgen

Proof of Theorem rgen
StepHypRef Expression
1 df-ral 2305 . 2
2 rgen.1 . 2
31, 2mpgbir 1339 1
Colors of variables: wff set class
Syntax hints:   wi 4   wcel 1390  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-gen 1335
This theorem depends on definitions:  df-bi 110  df-ral 2305
This theorem is referenced by:  rgen2a  2369  rgenw  2370  mprg  2372  mprgbir  2373  rgen2  2399  r19.21be  2404  nrex  2405  rexlimi  2420  sbcth2  2839  reuss  3212  ral0  3316  unimax  3605  mpteq1  3832  mpteq2ia  3834  ordon  4178  tfis  4249  finds  4266  finds2  4267  ordom  4272  fnopab  4966  fmpti  5264  opabex3  5691  indpi  6326  nnssre  7699  nnind  7711  nnsub  7733  dfuzi  8124  indstr  8312  cnref1o  8357  bj-indint  9386  bj-nnelirr  9407  bj-omord  9412
  Copyright terms: Public domain W3C validator