Theorem rgen 2603

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   A.wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1502

This proof depends on definitions:  df-bi 117  df-ral 2533

This theorem is used by:  rgen2a  2604  rgenw  2605  mprg  2607  mprgbir  2608  rgen2  2636  r19.21be  2641  nrex  2642  rexlimi  2661  sbcth2  3140  reuss  3514  ral0  3629  unimax  3969  mpteq1  4215  mpteq2ia  4217  ordon  4633  tfis  4730  finds  4747  finds2  4748  ordom  4754  omsinds  4769  dmxpid  5003  fnopab  5508  fmpti  5860  opabex3  6351  oawordriexmid  6743  fifo  7314  inresflem  7401  0ct  7448  infnninf  7465  infnninfOLD  7466  exmidonfinlem  7546  pw1on  7586  netap  7621  2omotaplemap  7624  indpi  7710  nnindnn  8261  aptap  8981  sup3exmid  9290  nnssre  9311  nnind  9323  nnsub  9346  dfuzi  9761  indstr  10003  cnref1o  10062  frec2uzsucd  10853  uzsinds  10896  ser0f  10986  bccl  11221  hashfibc  11299  wrdind  11510  rexuz3  11772  isumlessdc  12282  prodf1f  12329  iprodap0  12368  eff2  12466  reeff1  12486  prmind2  12917  3prm  12925  sqrt2irr  12960  phisum  13042  pockthi  13160  1arith  13169  1arith2  13170  prmlem1a  13244  ballotfilemofi  13271  ballotfilem2  13280  ballotfilemefi  13289  ballotfilemafi  13290  ballotfilembfi  13291  ballotfilem7  13331  prminf  13398  xpsff1o  13723  rngmgpf  14320  mgpf  14399  cnfld1  14993  cnsubglem  15000  isbasis3g  15238  distop  15277  cdivcncfap  15796  dveflem  15918  ioocosf1o  16047  2irrexpqap  16175  chtqub  16257  2sqlem6  16405  2sqlem10  16410  konigsberglem5  16899  bj-indint  17123  bj-nnelirr  17145  bj-omord  17152  012of  17189  2o01f  17190  0nninf  17213  nconstwlpolem0  17280