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  8942  sup3exmid  9251  nnssre  9261  nnind  9273  nnsub  9296  dfuzi  9709  indstr  9946  cnref1o  10004  frec2uzsucd  10790  uzsinds  10833  ser0f  10923  bccl  11157  hashfibc  11235  wrdind  11442  rexuz3  11704  isumlessdc  12211  prodf1f  12258  iprodap0  12297  eff2  12395  reeff1  12415  prmind2  12846  3prm  12854  sqrt2irr  12888  phisum  12967  pockthi  13085  1arith  13094  1arith2  13095  ballotfilemofi  13167  ballotfilem2  13176  ballotfilemefi  13185  ballotfilemafi  13186  ballotfilembfi  13187  ballotfilem7  13227  prminf  13294  xpsff1o  13617  rngmgpf  14180  mgpf  14258  cnfld1  14850  cnsubglem  14857  isbasis3g  15041  distop  15080  cdivcncfap  15599  dveflem  15721  ioocosf1o  15849  2irrexpqap  15973  2sqlem6  16123  2sqlem10  16128  konigsberglem5  16617  bj-indint  16841  bj-nnelirr  16863  bj-omord  16870  012of  16907  2o01f  16908  0nninf  16922  nconstwlpolem0  16988