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  7400  0ct  7447  infnninf  7464  infnninfOLD  7465  exmidonfinlem  7545  pw1on  7585  netap  7620  2omotaplemap  7623  indpi  7709  nnindnn  8260  aptap  8980  sup3exmid  9289  nnssre  9310  nnind  9322  nnsub  9345  dfuzi  9760  indstr  10002  cnref1o  10061  frec2uzsucd  10851  uzsinds  10894  ser0f  10984  bccl  11219  hashfibc  11297  wrdind  11508  rexuz3  11770  isumlessdc  12279  prodf1f  12326  iprodap0  12365  eff2  12463  reeff1  12483  prmind2  12914  3prm  12922  sqrt2irr  12957  phisum  13039  pockthi  13157  1arith  13166  1arith2  13167  prmlem1a  13241  ballotfilemofi  13268  ballotfilem2  13277  ballotfilemefi  13286  ballotfilemafi  13287  ballotfilembfi  13288  ballotfilem7  13328  prminf  13395  xpsff1o  13719  rngmgpf  14285  mgpf  14364  cnfld1  14958  cnsubglem  14965  isbasis3g  15196  distop  15235  cdivcncfap  15754  dveflem  15876  ioocosf1o  16005  2irrexpqap  16133  2sqlem6  16337  2sqlem10  16342  konigsberglem5  16831  bj-indint  17055  bj-nnelirr  17077  bj-omord  17084  012of  17121  2o01f  17122  0nninf  17145  nconstwlpolem0  17211