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

Theorem rgenw 2430
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 2428 1 𝑥𝐴 𝜑
Colors of variables: wff set class
Syntax hints:  wcel 1438  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  3840  iinexgm  3988  epse  4167  xpiindim  4569  eliunxp  4571  opeliunxp2  4572  elrnmpti  4684  fnmpti  5136  mpt2eq12  5701  iunex  5886  mpt2ex  5972  opeliunxp2f  5995  1domsn  6525  nneneq  6563  nqprrnd  7092  nqprdisj  7093  uzf  9012  sum0  10767  fisumcom2  10819  unennn  11475  bj-indint  11709  bj-nn0suc0  11728  bj-nntrans  11729
  Copyright terms: Public domain W3C validator