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

Theorem rgenw 2430
Description: Generalization rule for restricted quantification. (Contributed by NM, 18-Jun-2014.)
Hypothesis
Ref Expression
rgenw.1  |-  ph
Assertion
Ref Expression
rgenw  |-  A. x  e.  A  ph

Proof of Theorem rgenw
StepHypRef Expression
1 rgenw.1 . . 3  |-  ph
21a1i 9 . 2  |-  ( x  e.  A  ->  ph )
32rgen 2428 1  |-  A. x  e.  A  ph
Colors of variables: wff set class
Syntax hints:    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:  rgen2w  2431  reuun1  3281  0disj  3842  iinexgm  3990  epse  4169  xpiindim  4573  eliunxp  4575  opeliunxp2  4576  elrnmpti  4688  fnmpti  5142  mpt2eq12  5709  iunex  5894  mpt2ex  5980  opeliunxp2f  6003  1domsn  6533  nneneq  6571  nqprrnd  7100  nqprdisj  7101  uzf  9020  sum0  10776  fisumcom2  10828  unennn  11484  bj-indint  11781  bj-nn0suc0  11800  bj-nntrans  11801
  Copyright terms: Public domain W3C validator