Theorem rgen 2597

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

Syntax hints:   → wi 4   ∈ wcel 2205  ∀wral 2522

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 1498

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

This theorem is referenced by:  rgen2a  2598  rgenw  2599  mprg  2601  mprgbir  2602  rgen2  2630  r19.21be  2635  nrex  2636  rexlimi  2655  sbcth2  3134  reuss  3506  ral0  3615  unimax  3953  mpteq1  4199  mpteq2ia  4201  ordon  4613  tfis  4710  finds  4727  finds2  4728  ordom  4734  omsinds  4749  dmxpid  4983  fnopab  5488  fmpti  5834  opabex3  6324  oawordriexmid  6716  fifo  7280  inresflem  7364  0ct  7411  infnninf  7428  infnninfOLD  7429  exmidonfinlem  7509  pw1on  7549  netap  7584  2omotaplemap  7587  indpi  7673  nnindnn  8224  aptap  8941  sup3exmid  9248  nnssre  9258  nnind  9270  nnsub  9293  dfuzi  9706  indstr  9943  cnref1o  10001  frec2uzsucd  10787  uzsinds  10830  ser0f  10920  bccl  11154  hashfibc  11232  wrdind  11439  rexuz3  11700  isumlessdc  12207  prodf1f  12254  iprodap0  12293  eff2  12391  reeff1  12411  prmind2  12842  3prm  12850  sqrt2irr  12884  phisum  12963  pockthi  13081  1arith  13090  1arith2  13091  ballotfilemofi  13163  ballotfilem2  13172  ballotfilemefi  13181  ballotfilemafi  13182  ballotfilembfi  13183  ballotfilem7  13223  prminf  13290  xpsff1o  13646  rngmgpf  14165  mgpf  14239  cnfld1  14832  cnsubglem  14839  isbasis3g  15023  distop  15062  cdivcncfap  15581  dveflem  15703  ioocosf1o  15831  2irrexpqap  15955  2sqlem6  16105  2sqlem10  16110  konigsberglem5  16599  bj-indint  16813  bj-nnelirr  16835  bj-omord  16842  012of  16879  2o01f  16880  0nninf  16894  nconstwlpolem0  16961