Theorem rgen 2485

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

Syntax hints:   → wi 4   ∈ wcel 1480  ∀wral 2416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1425

This theorem depends on definitions:  df-bi 116  df-ral 2421

This theorem is referenced by:  rgen2a  2486  rgenw  2487  mprg  2489  mprgbir  2490  rgen2  2518  r19.21be  2523  nrex  2524  rexlimi  2542  sbcth2  2996  reuss  3357  ral0  3464  unimax  3770  mpteq1  4012  mpteq2ia  4014  ordon  4402  tfis  4497  finds  4514  finds2  4515  ordom  4520  omsinds  4535  dmxpid  4760  fnopab  5247  fmpti  5572  opabex3  6020  oawordriexmid  6366  fifo  6868  inresflem  6945  0ct  6992  infnninf  7022  exmidonfinlem  7049  indpi  7153  nnindnn  7704  sup3exmid  8718  nnssre  8727  nnind  8739  nnsub  8762  dfuzi  9164  indstr  9391  cnref1o  9443  frec2uzsucd  10177  uzsinds  10218  ser0f  10291  bccl  10516  rexuz3  10765  isumlessdc  11268  prodf1f  11315  eff2  11389  reeff1  11410  prmind2  11804  3prm  11812  sqrt2irr  11843  isbasis3g  12216  distop  12257  cdivcncfap  12759  dveflem  12858  bj-indint  13132  bj-nnelirr  13154  bj-omord  13161  0nninf  13200  isomninnlem  13228