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  3921  mpteq1  4167  mpteq2ia  4169  ordon  4575  tfis  4672  finds  4689  finds2  4690  ordom  4696  omsinds  4711  dmxpid  4941  fnopab  5444  fmpti  5780  opabex3  6257  oawordriexmid  6606  fifo  7135  inresflem  7215  0ct  7262  infnninf  7279  infnninfOLD  7280  exmidonfinlem  7359  pw1on  7399  netap  7428  2omotaplemap  7431  indpi  7517  nnindnn  8068  aptap  8785  sup3exmid  9092  nnssre  9102  nnind  9114  nnsub  9137  dfuzi  9545  indstr  9776  cnref1o  9834  frec2uzsucd  10610  uzsinds  10653  ser0f  10743  bccl  10976  wrdind  11240  rexuz3  11487  isumlessdc  11993  prodf1f  12040  iprodap0  12079  eff2  12177  reeff1  12197  prmind2  12628  3prm  12636  sqrt2irr  12670  phisum  12749  pockthi  12867  1arith  12876  1arith2  12877  prminf  13012  xpsff1o  13368  rngmgpf  13886  mgpf  13960  cnfld1  14521  cnsubglem  14528  isbasis3g  14705  distop  14744  cdivcncfap  15263  dveflem  15385  ioocosf1o  15513  2irrexpqap  15637  2sqlem6  15784  2sqlem10  15789  bj-indint  16224  bj-nnelirr  16246  bj-omord  16253  012of  16288  2o01f  16289  0nninf  16301  nconstwlpolem0  16362