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

Theorem rgen 2543
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 2473 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 rgen.1 . 2 (𝑥𝐴𝜑)
31, 2mpgbir 1464 1 𝑥𝐴 𝜑
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 2160  wral 2468
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1460
This theorem depends on definitions:  df-bi 117  df-ral 2473
This theorem is referenced by:  rgen2a  2544  rgenw  2545  mprg  2547  mprgbir  2548  rgen2  2576  r19.21be  2581  nrex  2582  rexlimi  2600  sbcth2  3065  reuss  3431  ral0  3539  unimax  3858  mpteq1  4102  mpteq2ia  4104  ordon  4503  tfis  4600  finds  4617  finds2  4618  ordom  4624  omsinds  4639  dmxpid  4866  fnopab  5359  fmpti  5688  opabex3  6146  oawordriexmid  6494  fifo  7008  inresflem  7088  0ct  7135  infnninf  7151  infnninfOLD  7152  exmidonfinlem  7221  pw1on  7254  netap  7282  2omotaplemap  7285  indpi  7370  nnindnn  7921  aptap  8636  sup3exmid  8943  nnssre  8952  nnind  8964  nnsub  8987  dfuzi  9392  indstr  9622  cnref1o  9679  frec2uzsucd  10431  uzsinds  10472  ser0f  10545  bccl  10778  rexuz3  11030  isumlessdc  11535  prodf1f  11582  iprodap0  11621  eff2  11719  reeff1  11739  prmind2  12151  3prm  12159  sqrt2irr  12193  phisum  12271  pockthi  12389  1arith  12398  1arith2  12399  prminf  12505  xpsff1o  12822  rngmgpf  13288  mgpf  13362  cnfld1  13872  cnsubglem  13879  isbasis3g  13998  distop  14037  cdivcncfap  14539  dveflem  14639  ioocosf1o  14727  2irrexpqap  14848  2sqlem6  14920  2sqlem10  14925  bj-indint  15136  bj-nnelirr  15158  bj-omord  15165  012of  15199  2o01f  15200  0nninf  15207  nconstwlpolem0  15265
  Copyright terms: Public domain W3C validator