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  4216  mpteq2ia  4219  ordon  4635  tfis  4732  finds  4749  finds2  4750  ordom  4756  omsinds  4771  dmxpid  5005  fnopab  5511  fmpti  5863  opabex3  6355  oawordriexmid  6748  fifo  7319  inresflem  7406  0ct  7453  infnninf  7470  infnninfOLD  7471  exmidonfinlem  7551  pw1on  7591  netap  7626  2omotaplemap  7629  indpi  7715  nnindnn  8266  aptap  8986  sup3exmid  9295  nnssre  9317  nnind  9329  nnsub  9352  dfuzi  9766  indstr  10008  cnref1o  10067  frec2uzsucd  10858  uzsinds  10901  ser0f  10991  bccl  11226  hashfibc  11304  wrdind  11515  rexuz3  11777  isumlessdc  12287  prodf1f  12334  iprodap0  12373  eff2  12471  reeff1  12491  prmind2  12922  3prm  12930  sqrt2irr  12965  phisum  13047  pockthi  13165  1arith  13174  1arith2  13175  prmlem1a  13249  ballotfilemofi  13276  ballotfilem2  13285  ballotfilemefi  13294  ballotfilemafi  13295  ballotfilembfi  13296  ballotfilem7  13336  prminf  13403  xpsff1o  13728  rngmgpf  14342  mgpf  14421  cnfld1  15017  cnsubglem  15024  isbasis3g  15289  distop  15328  cdivcncfap  15847  dveflem  15969  ioocosf1o  16099  2irrexpqap  16231  chtqub  16313  2sqlem6  16461  2sqlem10  16466  konigsberglem5  16955  bj-indint  17179  bj-nnelirr  17201  bj-omord  17208  012of  17245  2o01f  17246  0nninf  17270  nconstwlpolem0  17337