Theorem rgen 2510

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

Syntax hints:   -> wi 4   e. wcel 2128   A.wral 2435

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 1429

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

This theorem is referenced by:  rgen2a  2511  rgenw  2512  mprg  2514  mprgbir  2515  rgen2  2543  r19.21be  2548  nrex  2549  rexlimi  2567  sbcth2  3024  reuss  3388  ral0  3495  unimax  3806  mpteq1  4048  mpteq2ia  4050  ordon  4444  tfis  4541  finds  4558  finds2  4559  ordom  4565  omsinds  4580  dmxpid  4806  fnopab  5293  fmpti  5618  opabex3  6067  oawordriexmid  6414  fifo  6921  inresflem  6998  0ct  7045  infnninf  7061  infnninfOLD  7062  exmidonfinlem  7122  pw1on  7155  indpi  7256  nnindnn  7807  sup3exmid  8822  nnssre  8831  nnind  8843  nnsub  8866  dfuzi  9268  indstr  9498  cnref1o  9552  frec2uzsucd  10293  uzsinds  10334  ser0f  10407  bccl  10634  rexuz3  10883  isumlessdc  11386  prodf1f  11433  iprodap0  11472  eff2  11570  reeff1  11590  prmind2  11988  3prm  11996  sqrt2irr  12027  phisum  12103  isbasis3g  12415  distop  12456  cdivcncfap  12958  dveflem  13058  ioocosf1o  13146  2irrexpqap  13266  bj-indint  13477  bj-nnelirr  13499  bj-omord  13506  012of  13538  2o01f  13539  0nninf  13547  nconstwlpolem0  13604