Theorem rgen 2523

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 2453	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		rgen.1	. 2 |- ( x e. A -> ph )
3	1, 2	mpgbir 1446	1 |- A. x e. A ph

Syntax hints:   -> wi 4   e. wcel 2141   A.wral 2448

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 1442

This theorem depends on definitions:  df-bi 116  df-ral 2453

This theorem is referenced by:  rgen2a  2524  rgenw  2525  mprg  2527  mprgbir  2528  rgen2  2556  r19.21be  2561  nrex  2562  rexlimi  2580  sbcth2  3042  reuss  3408  ral0  3516  unimax  3830  mpteq1  4073  mpteq2ia  4075  ordon  4470  tfis  4567  finds  4584  finds2  4585  ordom  4591  omsinds  4606  dmxpid  4832  fnopab  5322  fmpti  5648  opabex3  6101  oawordriexmid  6449  fifo  6957  inresflem  7037  0ct  7084  infnninf  7100  infnninfOLD  7101  exmidonfinlem  7170  pw1on  7203  indpi  7304  nnindnn  7855  sup3exmid  8873  nnssre  8882  nnind  8894  nnsub  8917  dfuzi  9322  indstr  9552  cnref1o  9609  frec2uzsucd  10357  uzsinds  10398  ser0f  10471  bccl  10701  rexuz3  10954  isumlessdc  11459  prodf1f  11506  iprodap0  11545  eff2  11643  reeff1  11663  prmind2  12074  3prm  12082  sqrt2irr  12116  phisum  12194  pockthi  12310  1arith  12319  1arith2  12320  prminf  12410  isbasis3g  12838  distop  12879  cdivcncfap  13381  dveflem  13481  ioocosf1o  13569  2irrexpqap  13690  2sqlem6  13750  2sqlem10  13755  bj-indint  13966  bj-nnelirr  13988  bj-omord  13995  012of  14028  2o01f  14029  0nninf  14037  nconstwlpolem0  14094