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

Theorem rgenw 2461
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 2459 1  |-  A. x  e.  A  ph
Colors of variables: wff set class
Syntax hints:    e. wcel 1463   A.wral 2390
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1408
This theorem depends on definitions:  df-bi 116  df-ral 2395
This theorem is referenced by:  rgen2w  2462  reuun1  3324  0disj  3892  iinexgm  4039  epse  4224  xpiindim  4636  eliunxp  4638  opeliunxp2  4639  elrnmpti  4752  fnmpti  5209  mpoeq12  5785  iunex  5975  mpoex  6065  opeliunxp2f  6089  ixpssmap  6580  1domsn  6666  nneneq  6704  nqprrnd  7299  nqprdisj  7300  uzf  9231  sum0  11049  fisumcom2  11099  unennn  11755  tgidm  12086  tgrest  12181  txbas  12269  reldvg  12603  dvfvalap  12605  bj-indint  12821  bj-nn0suc0  12840  bj-nntrans  12841
  Copyright terms: Public domain W3C validator