Theorem rgen 2583

Description: Generalization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)

Hypothesis

Ref	Expression
rgen.1	⊢ (𝑥 ∈ 𝐴 → 𝜑)

Assertion

Ref	Expression
rgen	⊢ ∀𝑥 ∈ 𝐴 𝜑

Proof of Theorem rgen

Step	Hyp	Ref	Expression
1		df-ral 2513	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2		rgen.1	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝜑)
3	1, 2	mpgbir 1499	1 ⊢ ∀𝑥 ∈ 𝐴 𝜑

Syntax hints:   → wi 4   ∈ wcel 2200  ∀wral 2508

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 1495

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

This theorem is referenced by:  rgen2a  2584  rgenw  2585  mprg  2587  mprgbir  2588  rgen2  2616  r19.21be  2621  nrex  2622  rexlimi  2641  sbcth2  3117  reuss  3485  ral0  3593  unimax  3922  mpteq1  4168  mpteq2ia  4170  ordon  4578  tfis  4675  finds  4692  finds2  4693  ordom  4699  omsinds  4714  dmxpid  4945  fnopab  5448  fmpti  5789  opabex3  6273  oawordriexmid  6624  fifo  7155  inresflem  7235  0ct  7282  infnninf  7299  infnninfOLD  7300  exmidonfinlem  7379  pw1on  7419  netap  7448  2omotaplemap  7451  indpi  7537  nnindnn  8088  aptap  8805  sup3exmid  9112  nnssre  9122  nnind  9134  nnsub  9157  dfuzi  9565  indstr  9796  cnref1o  9854  frec2uzsucd  10631  uzsinds  10674  ser0f  10764  bccl  10997  wrdind  11262  rexuz3  11509  isumlessdc  12015  prodf1f  12062  iprodap0  12101  eff2  12199  reeff1  12219  prmind2  12650  3prm  12658  sqrt2irr  12692  phisum  12771  pockthi  12889  1arith  12898  1arith2  12899  prminf  13034  xpsff1o  13390  rngmgpf  13908  mgpf  13982  cnfld1  14544  cnsubglem  14551  isbasis3g  14728  distop  14767  cdivcncfap  15286  dveflem  15408  ioocosf1o  15536  2irrexpqap  15660  2sqlem6  15807  2sqlem10  15812  bj-indint  16318  bj-nnelirr  16340  bj-omord  16347  012of  16386  2o01f  16387  0nninf  16400  nconstwlpolem0  16461