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

Theorem rgen 2417
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 2354 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 rgen.1 . 2 (𝑥𝐴𝜑)
31, 2mpgbir 1383 1 𝑥𝐴 𝜑
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1434  wral 2349
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 1379
This theorem depends on definitions:  df-bi 115  df-ral 2354
This theorem is referenced by:  rgen2a  2418  rgenw  2419  mprg  2421  mprgbir  2422  rgen2  2448  r19.21be  2453  nrex  2454  rexlimi  2471  sbcth2  2902  reuss  3252  ral0  3350  unimax  3643  mpteq1  3870  mpteq2ia  3872  ordon  4238  tfis  4332  finds  4349  finds2  4350  ordom  4355  fnopab  5054  fmpti  5353  opabex3  5780  oawordriexmid  6114  indpi  6594  nnindnn  7121  nnssre  8110  nnind  8122  nnsub  8144  dfuzi  8538  indstr  8762  cnref1o  8814  frec2uzsucd  9483  uzsinds  9518  iser0f  9569  bccl  9791  rexuz3  10014  prmind2  10646  3prm  10654  sqrt2irr  10685  bj-indint  10884  bj-nnelirr  10906  bj-omord  10913
  Copyright terms: Public domain W3C validator