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  3616  unimax  3954  mpteq1  4200  mpteq2ia  4202  ordon  4615  tfis  4712  finds  4729  finds2  4730  ordom  4736  omsinds  4751  dmxpid  4985  fnopab  5490  fmpti  5836  opabex3  6326  oawordriexmid  6718  fifo  7282  inresflem  7366  0ct  7413  infnninf  7430  infnninfOLD  7431  exmidonfinlem  7511  pw1on  7551  netap  7586  2omotaplemap  7589  indpi  7675  nnindnn  8226  aptap  8944  sup3exmid  9253  nnssre  9263  nnind  9275  nnsub  9298  dfuzi  9711  indstr  9948  cnref1o  10006  frec2uzsucd  10792  uzsinds  10835  ser0f  10925  bccl  11159  hashfibc  11237  wrdind  11444  rexuz3  11706  isumlessdc  12213  prodf1f  12260  iprodap0  12299  eff2  12397  reeff1  12417  prmind2  12848  3prm  12856  sqrt2irr  12890  phisum  12969  pockthi  13087  1arith  13096  1arith2  13097  ballotfilemofi  13169  ballotfilem2  13178  ballotfilemefi  13187  ballotfilemafi  13188  ballotfilembfi  13189  ballotfilem7  13229  prminf  13296  xpsff1o  13619  rngmgpf  14182  mgpf  14260  cnfld1  14852  cnsubglem  14859  isbasis3g  15043  distop  15082  cdivcncfap  15601  dveflem  15723  ioocosf1o  15851  2irrexpqap  15975  2sqlem6  16125  2sqlem10  16130  konigsberglem5  16619  bj-indint  16843  bj-nnelirr  16865  bj-omord  16872  012of  16909  2o01f  16910  0nninf  16924  nconstwlpolem0  16990