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

Syntax hints:   -> wi 4   e. wcel 2209   A.wral 2528

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1502

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

This theorem is referenced by:  rgen2a  2604  rgenw  2605  mprg  2607  mprgbir  2608  rgen2  2636  r19.21be  2641  nrex  2642  rexlimi  2661  sbcth2  3140  reuss  3514  ral0  3626  unimax  3964  mpteq1  4210  mpteq2ia  4212  ordon  4628  tfis  4725  finds  4742  finds2  4743  ordom  4749  omsinds  4764  dmxpid  4998  fnopab  5503  fmpti  5851  opabex3  6341  oawordriexmid  6733  fifo  7304  inresflem  7390  0ct  7437  infnninf  7454  infnninfOLD  7455  exmidonfinlem  7535  pw1on  7575  netap  7610  2omotaplemap  7613  indpi  7699  nnindnn  8250  aptap  8968  sup3exmid  9277  nnssre  9287  nnind  9299  nnsub  9322  dfuzi  9735  indstr  9972  cnref1o  10030  frec2uzsucd  10816  uzsinds  10859  ser0f  10949  bccl  11183  hashfibc  11261  wrdind  11472  rexuz3  11734  isumlessdc  12241  prodf1f  12288  iprodap0  12327  eff2  12425  reeff1  12445  prmind2  12876  3prm  12884  sqrt2irr  12918  phisum  12997  pockthi  13115  1arith  13124  1arith2  13125  ballotfilemofi  13197  ballotfilem2  13206  ballotfilemefi  13215  ballotfilemafi  13216  ballotfilembfi  13217  ballotfilem7  13257  prminf  13324  xpsff1o  13647  rngmgpf  14211  mgpf  14289  cnfld1  14881  cnsubglem  14888  isbasis3g  15070  distop  15109  cdivcncfap  15628  dveflem  15750  ioocosf1o  15878  2irrexpqap  16003  2sqlem6  16153  2sqlem10  16158  konigsberglem5  16647  bj-indint  16871  bj-nnelirr  16893  bj-omord  16900  012of  16937  2o01f  16938  0nninf  16952  nconstwlpolem0  17018