Theorem rgen 2416

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

Syntax hints:   -> wi 4   e. wcel 1433   A.wral 2348

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 1378

This theorem depends on definitions:  df-bi 115  df-ral 2353

This theorem is referenced by:  rgen2a  2417  rgenw  2418  mprg  2420  mprgbir  2421  rgen2  2447  r19.21be  2452  nrex  2453  rexlimi  2470  sbcth2  2901  reuss  3245  ral0  3342  unimax  3635  mpteq1  3862  mpteq2ia  3864  ordon  4230  tfis  4324  finds  4341  finds2  4342  ordom  4347  fnopab  5043  fmpti  5342  opabex3  5769  indpi  6532  nnindnn  7059  nnssre  8043  nnind  8055  nnsub  8077  dfuzi  8457  indstr  8681  cnref1o  8733  uzsinds  9428  iser0f  9472  bccl  9694  rexuz3  9876  prmind2  10502  3prm  10510  sqrt2irr  10541  bj-indint  10726  bj-nnelirr  10748  bj-omord  10755