Theorem rgen 2603

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ∀wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1502

This proof depends on definitions:  df-bi 117  df-ral 2533

This theorem is used by:  rgen2a  2604  rgenw  2605  mprg  2607  mprgbir  2608  rgen2  2636  r19.21be  2641  nrex  2642  rexlimi  2661  sbcth2  3140  reuss  3514  ral0  3629  unimax  3969  mpteq1  4216  mpteq2ia  4219  ordon  4635  tfis  4732  finds  4749  finds2  4750  ordom  4756  omsinds  4771  dmxpid  5005  fnopab  5511  fmpti  5863  opabex3  6355  oawordriexmid  6748  fifo  7320  inresflem  7407  0ct  7454  infnninf  7471  infnninfOLD  7472  exmidonfinlem  7552  pw1on  7592  netap  7627  2omotaplemap  7630  indpi  7716  nnindnn  8267  aptap  8987  sup3exmid  9296  nnssre  9318  nnind  9330  nnsub  9353  dfuzi  9767  indstr  10009  cnref1o  10068  frec2uzsucd  10859  uzsinds  10902  ser0f  10992  bccl  11227  hashfibc  11305  wrdind  11516  rexuz3  11778  isumlessdc  12288  prodf1f  12335  iprodap0  12374  eff2  12472  reeff1  12492  prmind2  12923  3prm  12931  sqrt2irr  12966  phisum  13048  pockthi  13166  1arith  13175  1arith2  13176  prmlem1a  13250  ballotfilemofi  13277  ballotfilem2  13286  ballotfilemefi  13295  ballotfilemafi  13296  ballotfilembfi  13297  ballotfilem7  13337  prminf  13404  xpsff1o  13729  rngmgpf  14343  mgpf  14422  cnfld1  15018  cnsubglem  15025  isbasis3g  15305  distop  15344  cdivcncfap  15863  dveflem  15985  ioocosf1o  16115  2irrexpqap  16247  chtqub  16329  2sqlem6  16477  2sqlem10  16482  konigsberglem5  16971  bj-indint  17195  bj-nnelirr  17217  bj-omord  17224  012of  17261  2o01f  17262  0nninf  17286  nconstwlpolem0  17353