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

Theorem rgenw 2370
Description: Generalization rule for restricted quantification. (Contributed by NM, 18-Jun-2014.)
Hypothesis
Ref Expression
rgenw.1 φ
Assertion
Ref Expression
rgenw x A φ

Proof of Theorem rgenw
StepHypRef Expression
1 rgenw.1 . . 3 φ
21a1i 9 . 2 (x Aφ)
32rgen 2368 1 x A φ
Colors of variables: wff set class
Syntax hints:   wcel 1390  wral 2300
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 1335
This theorem depends on definitions:  df-bi 110  df-ral 2305
This theorem is referenced by:  rgen2w  2371  reuun1  3213  0disj  3752  iinexgm  3899  epse  4064  xpiindim  4416  eliunxp  4418  opeliunxp2  4419  elrnmpti  4530  fnmpti  4970  mpt2eq12  5507  iunex  5692  mpt2ex  5778  nqprrnd  6526  nqprdisj  6527  uzf  8252  bj-indint  9390  bj-nn0suc0  9410  bj-nntrans  9411
  Copyright terms: Public domain W3C validator