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

Theorem rgen 2462
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 2398 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 rgen.1 . 2 (𝑥𝐴𝜑)
31, 2mpgbir 1414 1 𝑥𝐴 𝜑
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1465  wral 2393
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1410
This theorem depends on definitions:  df-bi 116  df-ral 2398
This theorem is referenced by:  rgen2a  2463  rgenw  2464  mprg  2466  mprgbir  2467  rgen2  2495  r19.21be  2500  nrex  2501  rexlimi  2519  sbcth2  2968  reuss  3327  ral0  3434  unimax  3740  mpteq1  3982  mpteq2ia  3984  ordon  4372  tfis  4467  finds  4484  finds2  4485  ordom  4490  omsinds  4505  dmxpid  4730  fnopab  5217  fmpti  5540  opabex3  5988  oawordriexmid  6334  fifo  6836  inresflem  6913  0ct  6960  infnninf  6990  exmidonfinlem  7017  indpi  7118  nnindnn  7669  sup3exmid  8683  nnssre  8692  nnind  8704  nnsub  8727  dfuzi  9129  indstr  9356  cnref1o  9408  frec2uzsucd  10142  uzsinds  10183  ser0f  10256  bccl  10481  rexuz3  10730  isumlessdc  11233  eff2  11313  reeff1  11334  prmind2  11728  3prm  11736  sqrt2irr  11767  isbasis3g  12140  distop  12181  cdivcncfap  12683  dveflem  12782  bj-indint  13056  bj-nnelirr  13078  bj-omord  13085  0nninf  13124  isomninnlem  13152
  Copyright terms: Public domain W3C validator