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

Theorem rgen 2428
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 2364 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 rgen.1 . 2  |-  ( x  e.  A  ->  ph )
31, 2mpgbir 1387 1  |-  A. x  e.  A  ph
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1438   A.wral 2359
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1383
This theorem depends on definitions:  df-bi 115  df-ral 2364
This theorem is referenced by:  rgen2a  2429  rgenw  2430  mprg  2432  mprgbir  2433  rgen2  2459  r19.21be  2464  nrex  2465  rexlimi  2482  sbcth2  2924  reuss  3278  ral0  3379  unimax  3682  mpteq1  3914  mpteq2ia  3916  ordon  4293  tfis  4388  finds  4405  finds2  4406  ordom  4411  omsinds  4425  fnopab  5124  fmpti  5435  opabex3  5875  oawordriexmid  6213  inresflem  6731  infnninf  6784  indpi  6880  nnindnn  7407  nnssre  8398  nnind  8410  nnsub  8432  dfuzi  8826  indstr  9050  cnref1o  9102  frec2uzsucd  9773  uzsinds  9813  iser0f  9913  ser0f  9915  bccl  10140  rexuz3  10388  prmind2  11195  3prm  11203  sqrt2irr  11234  bj-indint  11483  bj-nnelirr  11505  bj-omord  11512  0nninf  11550
  Copyright terms: Public domain W3C validator