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

Theorem rgen 2428
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 2364 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 rgen.1 . 2 (𝑥𝐴𝜑)
31, 2mpgbir 1387 1 𝑥𝐴 𝜑
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1438  wral 2359
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1383
This theorem depends on definitions:  df-bi 115  df-ral 2364
This theorem is referenced by:  rgen2a  2429  rgenw  2430  mprg  2432  mprgbir  2433  rgen2  2459  r19.21be  2464  nrex  2465  rexlimi  2482  sbcth2  2924  reuss  3278  ral0  3379  unimax  3682  mpteq1  3914  mpteq2ia  3916  ordon  4293  tfis  4388  finds  4405  finds2  4406  ordom  4411  omsinds  4425  fnopab  5124  fmpti  5435  opabex3  5875  oawordriexmid  6213  inresflem  6731  infnninf  6784  indpi  6880  nnindnn  7407  nnssre  8398  nnind  8410  nnsub  8432  dfuzi  8826  indstr  9050  cnref1o  9102  frec2uzsucd  9773  uzsinds  9813  iser0f  9913  ser0f  9915  bccl  10140  rexuz3  10388  prmind2  11184  3prm  11192  sqrt2irr  11223  bj-indint  11472  bj-nnelirr  11494  bj-omord  11501  0nninf  11539
  Copyright terms: Public domain W3C validator