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

Theorem rgenw 2462
Description: Generalization rule for restricted quantification. (Contributed by NM, 18-Jun-2014.)
Hypothesis
Ref Expression
rgenw.1 𝜑
Assertion
Ref Expression
rgenw 𝑥𝐴 𝜑

Proof of Theorem rgenw
StepHypRef Expression
1 rgenw.1 . . 3 𝜑
21a1i 9 . 2 (𝑥𝐴𝜑)
32rgen 2460 1 𝑥𝐴 𝜑
Colors of variables: wff set class
Syntax hints:  wcel 1463  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:  rgen2w  2463  reuun1  3326  0disj  3894  iinexgm  4047  epse  4232  xpiindim  4644  eliunxp  4646  opeliunxp2  4647  elrnmpti  4760  fnmpti  5219  mpoeq12  5797  iunex  5987  mpoex  6077  opeliunxp2f  6101  ixpssmap  6592  1domsn  6679  nneneq  6717  nqprrnd  7315  nqprdisj  7316  uzf  9281  sum0  11108  fisumcom2  11158  unennn  11816  tgidm  12149  tgrest  12244  txbas  12333  reldvg  12723  dvfvalap  12725  bj-indint  12963  bj-nn0suc0  12982  bj-nntrans  12983
  Copyright terms: Public domain W3C validator