Theorem rgen 2547

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

Syntax hints:   -> wi 4   e. wcel 2164   A.wral 2472

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 1460

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

This theorem is referenced by:  rgen2a  2548  rgenw  2549  mprg  2551  mprgbir  2552  rgen2  2580  r19.21be  2585  nrex  2586  rexlimi  2604  sbcth2  3073  reuss  3440  ral0  3548  unimax  3869  mpteq1  4113  mpteq2ia  4115  ordon  4518  tfis  4615  finds  4632  finds2  4633  ordom  4639  omsinds  4654  dmxpid  4883  fnopab  5378  fmpti  5710  opabex3  6174  oawordriexmid  6523  fifo  7039  inresflem  7119  0ct  7166  infnninf  7183  infnninfOLD  7184  exmidonfinlem  7253  pw1on  7286  netap  7314  2omotaplemap  7317  indpi  7402  nnindnn  7953  aptap  8669  sup3exmid  8976  nnssre  8986  nnind  8998  nnsub  9021  dfuzi  9427  indstr  9658  cnref1o  9716  frec2uzsucd  10472  uzsinds  10515  ser0f  10605  bccl  10838  rexuz3  11134  isumlessdc  11639  prodf1f  11686  iprodap0  11725  eff2  11823  reeff1  11843  prmind2  12258  3prm  12266  sqrt2irr  12300  phisum  12378  pockthi  12496  1arith  12505  1arith2  12506  prminf  12612  xpsff1o  12932  rngmgpf  13433  mgpf  13507  cnfld1  14060  cnsubglem  14067  isbasis3g  14214  distop  14253  cdivcncfap  14758  dveflem  14872  ioocosf1o  14989  2irrexpqap  15110  2sqlem6  15207  2sqlem10  15212  bj-indint  15423  bj-nnelirr  15445  bj-omord  15452  012of  15486  2o01f  15487  0nninf  15494  nconstwlpolem0  15553