Theorem rgen 2586

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

Syntax hints:   → wi 4   ∈ wcel 2202  ∀wral 2511

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 2516

This theorem is referenced by:  rgen2a  2587  rgenw  2588  mprg  2590  mprgbir  2591  rgen2  2619  r19.21be  2624  nrex  2625  rexlimi  2644  sbcth2  3121  reuss  3490  ral0  3598  unimax  3932  mpteq1  4178  mpteq2ia  4180  ordon  4590  tfis  4687  finds  4704  finds2  4705  ordom  4711  omsinds  4726  dmxpid  4959  fnopab  5464  fmpti  5807  opabex3  6293  oawordriexmid  6681  fifo  7222  inresflem  7302  0ct  7349  infnninf  7366  infnninfOLD  7367  exmidonfinlem  7447  pw1on  7487  netap  7516  2omotaplemap  7519  indpi  7605  nnindnn  8156  aptap  8873  sup3exmid  9180  nnssre  9190  nnind  9202  nnsub  9225  dfuzi  9633  indstr  9870  cnref1o  9928  frec2uzsucd  10707  uzsinds  10750  ser0f  10840  bccl  11073  wrdind  11350  rexuz3  11611  isumlessdc  12118  prodf1f  12165  iprodap0  12204  eff2  12302  reeff1  12322  prmind2  12753  3prm  12761  sqrt2irr  12795  phisum  12874  pockthi  12992  1arith  13001  1arith2  13002  prminf  13137  xpsff1o  13493  rngmgpf  14012  mgpf  14086  cnfld1  14648  cnsubglem  14655  isbasis3g  14837  distop  14876  cdivcncfap  15395  dveflem  15517  ioocosf1o  15645  2irrexpqap  15769  2sqlem6  15919  2sqlem10  15924  konigsberglem5  16413  bj-indint  16627  bj-nnelirr  16649  bj-omord  16656  012of  16693  2o01f  16694  0nninf  16710  nconstwlpolem0  16776