NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  rgen GIF version

Theorem rgen 2679
Description: Generalization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)
Hypothesis
Ref Expression
rgen.1 (x Aφ)
Assertion
Ref Expression
rgen x A φ

Proof of Theorem rgen
StepHypRef Expression
1 df-ral 2619 . 2 (x A φx(x Aφ))
2 rgen.1 . 2 (x Aφ)
31, 2mpgbir 1550 1 x A φ
Colors of variables: wff setvar class
Syntax hints:  wi 4   wcel 1710  wral 2614
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546
This theorem depends on definitions:  df-bi 177  df-ral 2619
This theorem is referenced by:  rgen2a  2680  rgenw  2681  mprg  2683  mprgbir  2684  rgen2  2710  r19.21be  2715  nrex  2716  rexlimi  2731  sbcth2  3129  reuss  3536  r19.2zb  3640  ral0  3654  unimax  3925  nndisjeq  4429  fnopab  5207  mpteq1  5658  mpteq2ia  5659  fmpti  5693  clos1is  5881  nclenn  6249  nmembers1lem2  6269  nnc3n3p1  6278  nchoicelem12  6300
  Copyright terms: Public domain W3C validator