Theorem rgen 2374

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

Syntax hints:   -> wi 4   e. wcel 1393   A.wral 2306

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1338

This theorem depends on definitions:  df-bi 110  df-ral 2311

This theorem is referenced by:  rgen2a  2375  rgenw  2376  mprg  2378  mprgbir  2379  rgen2  2405  r19.21be  2410  nrex  2411  rexlimi  2426  sbcth2  2845  reuss  3218  ral0  3322  unimax  3614  mpteq1  3841  mpteq2ia  3843  ordon  4212  tfis  4306  finds  4323  finds2  4324  ordom  4329  fnopab  5023  fmpti  5321  opabex3  5749  indpi  6440  nnindnn  6967  nnssre  7918  nnind  7930  nnsub  7952  dfuzi  8348  indstr  8536  cnref1o  8582  iser0f  9251  rexuz3  9588  sqrt2irr  9878  bj-indint  10055  bj-nnelirr  10078  bj-omord  10085