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  8978  sup3exmid  9287  nnssre  9308  nnind  9320  nnsub  9343  dfuzi  9756  indstr  9993  cnref1o  10051  frec2uzsucd  10838  uzsinds  10881  ser0f  10971  bccl  11205  hashfibc  11283  wrdind  11494  rexuz3  11756  isumlessdc  12263  prodf1f  12310  iprodap0  12349  eff2  12447  reeff1  12467  prmind2  12898  3prm  12906  sqrt2irr  12940  phisum  13019  pockthi  13137  1arith  13146  1arith2  13147  ballotfilemofi  13219  ballotfilem2  13228  ballotfilemefi  13237  ballotfilemafi  13238  ballotfilembfi  13239  ballotfilem7  13279  prminf  13346  xpsff1o  13670  rngmgpf  14236  mgpf  14315  cnfld1  14909  cnsubglem  14916  isbasis3g  15147  distop  15186  cdivcncfap  15705  dveflem  15827  ioocosf1o  15955  2irrexpqap  16080  2sqlem6  16239  2sqlem10  16244  konigsberglem5  16733  bj-indint  16957  bj-nnelirr  16979  bj-omord  16986  012of  17023  2o01f  17024  0nninf  17047  nconstwlpolem0  17113