Theorem rgen 2530

Description: Generalization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)

Hypothesis

Ref	Expression
rgen.1	|- ( x e. A -> ph )

Assertion

Ref	Expression
rgen	|- A. x e. A ph

Proof of Theorem rgen

Step	Hyp	Ref	Expression
1		df-ral 2460	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		rgen.1	. 2 |- ( x e. A -> ph )
3	1, 2	mpgbir 1453	1 |- A. x e. A ph

Syntax hints:   -> wi 4   e. wcel 2148   A.wral 2455

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 1449

This theorem depends on definitions:  df-bi 117  df-ral 2460

This theorem is referenced by:  rgen2a  2531  rgenw  2532  mprg  2534  mprgbir  2535  rgen2  2563  r19.21be  2568  nrex  2569  rexlimi  2587  sbcth2  3052  reuss  3418  ral0  3526  unimax  3845  mpteq1  4089  mpteq2ia  4091  ordon  4487  tfis  4584  finds  4601  finds2  4602  ordom  4608  omsinds  4623  dmxpid  4850  fnopab  5342  fmpti  5671  opabex3  6126  oawordriexmid  6474  fifo  6982  inresflem  7062  0ct  7109  infnninf  7125  infnninfOLD  7126  exmidonfinlem  7195  pw1on  7228  netap  7256  2omotaplemap  7259  indpi  7344  nnindnn  7895  aptap  8610  sup3exmid  8917  nnssre  8926  nnind  8938  nnsub  8961  dfuzi  9366  indstr  9596  cnref1o  9653  frec2uzsucd  10404  uzsinds  10445  ser0f  10518  bccl  10750  rexuz3  11002  isumlessdc  11507  prodf1f  11554  iprodap0  11593  eff2  11691  reeff1  11711  prmind2  12123  3prm  12131  sqrt2irr  12165  phisum  12243  pockthi  12359  1arith  12368  1arith2  12369  prminf  12459  xpsff1o  12775  mgpf  13205  cnfld1  13613  cnsubglem  13620  isbasis3g  13707  distop  13746  cdivcncfap  14248  dveflem  14348  ioocosf1o  14436  2irrexpqap  14557  2sqlem6  14628  2sqlem10  14633  bj-indint  14844  bj-nnelirr  14866  bj-omord  14873  012of  14907  2o01f  14908  0nninf  14915  nconstwlpolem0  14973