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  3118  reuss  3486  ral0  3594  unimax  3925  mpteq1  4171  mpteq2ia  4173  ordon  4582  tfis  4679  finds  4696  finds2  4697  ordom  4703  omsinds  4718  dmxpid  4951  fnopab  5454  fmpti  5795  opabex3  6279  oawordriexmid  6633  fifo  7173  inresflem  7253  0ct  7300  infnninf  7317  infnninfOLD  7318  exmidonfinlem  7397  pw1on  7437  netap  7466  2omotaplemap  7469  indpi  7555  nnindnn  8106  aptap  8823  sup3exmid  9130  nnssre  9140  nnind  9152  nnsub  9175  dfuzi  9583  indstr  9820  cnref1o  9878  frec2uzsucd  10656  uzsinds  10699  ser0f  10789  bccl  11022  wrdind  11296  rexuz3  11544  isumlessdc  12050  prodf1f  12097  iprodap0  12136  eff2  12234  reeff1  12254  prmind2  12685  3prm  12693  sqrt2irr  12727  phisum  12806  pockthi  12924  1arith  12933  1arith2  12934  prminf  13069  xpsff1o  13425  rngmgpf  13943  mgpf  14017  cnfld1  14579  cnsubglem  14586  isbasis3g  14763  distop  14802  cdivcncfap  15321  dveflem  15443  ioocosf1o  15571  2irrexpqap  15695  2sqlem6  15842  2sqlem10  15847  bj-indint  16476  bj-nnelirr  16498  bj-omord  16505  012of  16542  2o01f  16543  0nninf  16556  nconstwlpolem0  16617