Theorem rgen 2586

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

Syntax hints:   -> wi 4   e. wcel 2202   A.wral 2511

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 1498

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

This theorem is referenced by:  rgen2a  2587  rgenw  2588  mprg  2590  mprgbir  2591  rgen2  2619  r19.21be  2624  nrex  2625  rexlimi  2644  sbcth2  3121  reuss  3490  ral0  3598  unimax  3932  mpteq1  4178  mpteq2ia  4180  ordon  4590  tfis  4687  finds  4704  finds2  4705  ordom  4711  omsinds  4726  dmxpid  4959  fnopab  5464  fmpti  5807  opabex3  6293  oawordriexmid  6681  fifo  7239  inresflem  7319  0ct  7366  infnninf  7383  infnninfOLD  7384  exmidonfinlem  7464  pw1on  7504  netap  7533  2omotaplemap  7536  indpi  7622  nnindnn  8173  aptap  8889  sup3exmid  9196  nnssre  9206  nnind  9218  nnsub  9241  dfuzi  9651  indstr  9888  cnref1o  9946  frec2uzsucd  10726  uzsinds  10769  ser0f  10859  bccl  11092  wrdind  11369  rexuz3  11630  isumlessdc  12137  prodf1f  12184  iprodap0  12223  eff2  12321  reeff1  12341  prmind2  12772  3prm  12780  sqrt2irr  12814  phisum  12893  pockthi  13011  1arith  13020  1arith2  13021  prminf  13156  xpsff1o  13512  rngmgpf  14031  mgpf  14105  cnfld1  14668  cnsubglem  14675  isbasis3g  14857  distop  14896  cdivcncfap  15415  dveflem  15537  ioocosf1o  15665  2irrexpqap  15789  2sqlem6  15939  2sqlem10  15944  konigsberglem5  16433  bj-indint  16647  bj-nnelirr  16669  bj-omord  16676  012of  16713  2o01f  16714  0nninf  16730  nconstwlpolem0  16796