Theorem rgen 2585

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 2515	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2		rgen.1	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝜑)
3	1, 2	mpgbir 1501	1 ⊢ ∀𝑥 ∈ 𝐴 𝜑

Syntax hints:   → wi 4   ∈ wcel 2202  ∀wral 2510

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 1497

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

This theorem is referenced by:  rgen2a  2586  rgenw  2587  mprg  2589  mprgbir  2590  rgen2  2618  r19.21be  2623  nrex  2624  rexlimi  2643  sbcth2  3120  reuss  3488  ral0  3596  unimax  3927  mpteq1  4173  mpteq2ia  4175  ordon  4584  tfis  4681  finds  4698  finds2  4699  ordom  4705  omsinds  4720  dmxpid  4953  fnopab  5457  fmpti  5799  opabex3  6284  oawordriexmid  6638  fifo  7179  inresflem  7259  0ct  7306  infnninf  7323  infnninfOLD  7324  exmidonfinlem  7404  pw1on  7444  netap  7473  2omotaplemap  7476  indpi  7562  nnindnn  8113  aptap  8830  sup3exmid  9137  nnssre  9147  nnind  9159  nnsub  9182  dfuzi  9590  indstr  9827  cnref1o  9885  frec2uzsucd  10664  uzsinds  10707  ser0f  10797  bccl  11030  wrdind  11307  rexuz3  11555  isumlessdc  12062  prodf1f  12109  iprodap0  12148  eff2  12246  reeff1  12266  prmind2  12697  3prm  12705  sqrt2irr  12739  phisum  12818  pockthi  12936  1arith  12945  1arith2  12946  prminf  13081  xpsff1o  13437  rngmgpf  13956  mgpf  14030  cnfld1  14592  cnsubglem  14599  isbasis3g  14776  distop  14815  cdivcncfap  15334  dveflem  15456  ioocosf1o  15584  2irrexpqap  15708  2sqlem6  15855  2sqlem10  15860  bj-indint  16552  bj-nnelirr  16574  bj-omord  16581  012of  16618  2o01f  16619  0nninf  16632  nconstwlpolem0  16693