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

Theorem rgen 2391
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 2328 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 rgen.1 . 2  |-  ( x  e.  A  ->  ph )
31, 2mpgbir 1358 1  |-  A. x  e.  A  ph
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1409   A.wral 2323
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-gen 1354
This theorem depends on definitions:  df-bi 114  df-ral 2328
This theorem is referenced by:  rgen2a  2392  rgenw  2393  mprg  2395  mprgbir  2396  rgen2  2422  r19.21be  2427  nrex  2428  rexlimi  2443  sbcth2  2873  reuss  3246  ral0  3350  unimax  3642  mpteq1  3869  mpteq2ia  3871  ordon  4240  tfis  4334  finds  4351  finds2  4352  ordom  4357  fnopab  5051  fmpti  5349  opabex3  5777  indpi  6498  nnindnn  7025  nnssre  7994  nnind  8006  nnsub  8028  dfuzi  8407  indstr  8632  cnref1o  8680  iser0f  9416  bccl  9635  rexuz3  9817  sqrt2irr  10251  bj-indint  10442  bj-nnelirr  10465  bj-omord  10472
  Copyright terms: Public domain W3C validator