Theorem rgen 2559

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

Syntax hints:   -> wi 4   e. wcel 2176   A.wral 2484

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 1472

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

This theorem is referenced by:  rgen2a  2560  rgenw  2561  mprg  2563  mprgbir  2564  rgen2  2592  r19.21be  2597  nrex  2598  rexlimi  2616  sbcth2  3086  reuss  3454  ral0  3562  unimax  3884  mpteq1  4128  mpteq2ia  4130  ordon  4534  tfis  4631  finds  4648  finds2  4649  ordom  4655  omsinds  4670  dmxpid  4899  fnopab  5400  fmpti  5732  opabex3  6207  oawordriexmid  6556  fifo  7082  inresflem  7162  0ct  7209  infnninf  7226  infnninfOLD  7227  exmidonfinlem  7301  pw1on  7338  netap  7366  2omotaplemap  7369  indpi  7455  nnindnn  8006  aptap  8723  sup3exmid  9030  nnssre  9040  nnind  9052  nnsub  9075  dfuzi  9483  indstr  9714  cnref1o  9772  frec2uzsucd  10546  uzsinds  10589  ser0f  10679  bccl  10912  rexuz3  11301  isumlessdc  11807  prodf1f  11854  iprodap0  11893  eff2  11991  reeff1  12011  prmind2  12442  3prm  12450  sqrt2irr  12484  phisum  12563  pockthi  12681  1arith  12690  1arith2  12691  prminf  12826  xpsff1o  13181  rngmgpf  13699  mgpf  13773  cnfld1  14334  cnsubglem  14341  isbasis3g  14518  distop  14557  cdivcncfap  15076  dveflem  15198  ioocosf1o  15326  2irrexpqap  15450  2sqlem6  15597  2sqlem10  15602  bj-indint  15867  bj-nnelirr  15889  bj-omord  15896  012of  15930  2o01f  15931  0nninf  15941  nconstwlpolem0  16002