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

Theorem rgen 2374
 Description: Generalization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)
Hypothesis
Ref Expression
rgen.1 (𝑥𝐴𝜑)
Assertion
Ref Expression
rgen 𝑥𝐴 𝜑

Proof of Theorem rgen
StepHypRef Expression
1 df-ral 2311 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 rgen.1 . 2 (𝑥𝐴𝜑)
31, 2mpgbir 1342 1 𝑥𝐴 𝜑
 Colors of variables: wff set class Syntax hints:   → wi 4   ∈ 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:  rgen2a  2375  rgenw  2376  mprg  2378  mprgbir  2379  rgen2  2405  r19.21be  2410  nrex  2411  rexlimi  2426  sbcth2  2845  reuss  3218  ral0  3322  unimax  3614  mpteq1  3841  mpteq2ia  3843  ordon  4212  tfis  4306  finds  4323  finds2  4324  ordom  4329  fnopab  5023  fmpti  5321  opabex3  5749  indpi  6440  nnindnn  6967  nnssre  7918  nnind  7930  nnsub  7952  dfuzi  8348  indstr  8536  cnref1o  8582  iser0f  9251  rexuz3  9588  sqrt2irr  9878  bj-indint  10055  bj-nnelirr  10078  bj-omord  10085
 Copyright terms: Public domain W3C validator