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

Theorem rgen 2460
Description: Generalization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)
Hypothesis
Ref Expression
rgen.1  |-  ( x  e.  A  ->  ph )
Assertion
Ref Expression
rgen  |-  A. x  e.  A  ph

Proof of Theorem rgen
StepHypRef Expression
1 df-ral 2396 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 rgen.1 . 2  |-  ( x  e.  A  ->  ph )
31, 2mpgbir 1412 1  |-  A. x  e.  A  ph
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1463   A.wral 2391
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-gen 1408
This theorem depends on definitions:  df-bi 116  df-ral 2396
This theorem is referenced by:  rgen2a  2461  rgenw  2462  mprg  2464  mprgbir  2465  rgen2  2493  r19.21be  2498  nrex  2499  rexlimi  2517  sbcth2  2966  reuss  3325  ral0  3432  unimax  3738  mpteq1  3980  mpteq2ia  3982  ordon  4370  tfis  4465  finds  4482  finds2  4483  ordom  4488  omsinds  4503  dmxpid  4728  fnopab  5215  fmpti  5538  opabex3  5986  oawordriexmid  6332  fifo  6834  inresflem  6911  0ct  6958  infnninf  6988  indpi  7114  nnindnn  7665  sup3exmid  8675  nnssre  8684  nnind  8696  nnsub  8719  dfuzi  9115  indstr  9340  cnref1o  9392  frec2uzsucd  10125  uzsinds  10166  ser0f  10239  bccl  10464  rexuz3  10713  isumlessdc  11216  eff2  11296  reeff1  11317  prmind2  11708  3prm  11716  sqrt2irr  11747  isbasis3g  12119  distop  12160  cdivcncfap  12662  dveflem  12761  bj-indint  12963  bj-nnelirr  12985  bj-omord  12992  0nninf  13031  isomninnlem  13059  sin24declemlt  13076
  Copyright terms: Public domain W3C validator