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

Theorem rgenw 2376
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 2374 1 𝑥𝐴 𝜑
Colors of variables: wff set class
Syntax hints:  wcel 1393  wral 2306
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1338
This theorem depends on definitions:  df-bi 110  df-ral 2311
This theorem is referenced by:  rgen2w  2377  reuun1  3219  0disj  3761  iinexgm  3908  epse  4079  xpiindim  4473  eliunxp  4475  opeliunxp2  4476  elrnmpti  4587  fnmpti  5027  mpt2eq12  5565  iunex  5750  mpt2ex  5836  nneneq  6320  nqprrnd  6639  nqprdisj  6640  uzf  8474  bj-indint  10029  bj-nn0suc0  10049  bj-nntrans  10050
  Copyright terms: Public domain W3C validator