Theorem rgen 2595

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

Syntax hints:   → wi 4   ∈ wcel 2203  ∀wral 2520

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 2525

This theorem is referenced by:  rgen2a  2596  rgenw  2597  mprg  2599  mprgbir  2600  rgen2  2628  r19.21be  2633  nrex  2634  rexlimi  2653  sbcth2  3130  reuss  3501  ral0  3610  unimax  3947  mpteq1  4193  mpteq2ia  4195  ordon  4607  tfis  4704  finds  4721  finds2  4722  ordom  4728  omsinds  4743  dmxpid  4977  fnopab  5482  fmpti  5828  opabex3  6314  oawordriexmid  6702  fifo  7266  inresflem  7350  0ct  7397  infnninf  7414  infnninfOLD  7415  exmidonfinlem  7495  pw1on  7535  netap  7567  2omotaplemap  7570  indpi  7656  nnindnn  8207  aptap  8923  sup3exmid  9230  nnssre  9240  nnind  9252  nnsub  9275  dfuzi  9687  indstr  9924  cnref1o  9982  frec2uzsucd  10762  uzsinds  10805  ser0f  10895  bccl  11128  hashfibc  11203  wrdind  11410  rexuz3  11671  isumlessdc  12178  prodf1f  12225  iprodap0  12264  eff2  12362  reeff1  12382  prmind2  12813  3prm  12821  sqrt2irr  12855  phisum  12934  pockthi  13052  1arith  13061  1arith2  13062  ballotfilemofi  13134  prminf  13198  xpsff1o  13554  rngmgpf  14073  mgpf  14147  cnfld1  14712  cnsubglem  14719  isbasis3g  14903  distop  14942  cdivcncfap  15461  dveflem  15583  ioocosf1o  15711  2irrexpqap  15835  2sqlem6  15985  2sqlem10  15990  konigsberglem5  16479  bj-indint  16693  bj-nnelirr  16715  bj-omord  16722  012of  16759  2o01f  16760  0nninf  16774  nconstwlpolem0  16840