Theorem rgen 2488

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

Syntax hints:   -> wi 4   e. wcel 1481   A.wral 2417

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 1426

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

This theorem is referenced by:  rgen2a  2489  rgenw  2490  mprg  2492  mprgbir  2493  rgen2  2521  r19.21be  2526  nrex  2527  rexlimi  2545  sbcth2  3000  reuss  3362  ral0  3469  unimax  3778  mpteq1  4020  mpteq2ia  4022  ordon  4410  tfis  4505  finds  4522  finds2  4523  ordom  4528  omsinds  4543  dmxpid  4768  fnopab  5255  fmpti  5580  opabex3  6028  oawordriexmid  6374  fifo  6876  inresflem  6953  0ct  7000  infnninf  7030  exmidonfinlem  7066  indpi  7174  nnindnn  7725  sup3exmid  8739  nnssre  8748  nnind  8760  nnsub  8783  dfuzi  9185  indstr  9415  cnref1o  9469  frec2uzsucd  10205  uzsinds  10246  ser0f  10319  bccl  10545  rexuz3  10794  isumlessdc  11297  prodf1f  11344  iprodap0  11383  eff2  11423  reeff1  11443  prmind2  11837  3prm  11845  sqrt2irr  11876  isbasis3g  12252  distop  12293  cdivcncfap  12795  dveflem  12895  ioocosf1o  12983  2irrexpqap  13103  bj-indint  13300  bj-nnelirr  13322  bj-omord  13329  012of  13363  2o01f  13364  0nninf  13372