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

Theorem rgenw 2393
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 2391 1 𝑥𝐴 𝜑
Colors of variables: wff set class
Syntax hints:  wcel 1409  wral 2323
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-gen 1354
This theorem depends on definitions:  df-bi 114  df-ral 2328
This theorem is referenced by:  rgen2w  2394  reuun1  3247  0disj  3789  iinexgm  3936  epse  4107  xpiindim  4501  eliunxp  4503  opeliunxp2  4504  elrnmpti  4615  fnmpti  5055  mpt2eq12  5593  iunex  5778  mpt2ex  5864  nneneq  6351  nqprrnd  6699  nqprdisj  6700  uzf  8572  bj-indint  10442  bj-nn0suc0  10462  bj-nntrans  10463
  Copyright terms: Public domain W3C validator