Theorem rgen 2519

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

Syntax hints:   → wi 4   ∈ wcel 2136  ∀wral 2444

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 1437

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

This theorem is referenced by:  rgen2a  2520  rgenw  2521  mprg  2523  mprgbir  2524  rgen2  2552  r19.21be  2557  nrex  2558  rexlimi  2576  sbcth2  3038  reuss  3403  ral0  3510  unimax  3823  mpteq1  4066  mpteq2ia  4068  ordon  4463  tfis  4560  finds  4577  finds2  4578  ordom  4584  omsinds  4599  dmxpid  4825  fnopab  5312  fmpti  5637  opabex3  6090  oawordriexmid  6438  fifo  6945  inresflem  7025  0ct  7072  infnninf  7088  infnninfOLD  7089  exmidonfinlem  7149  pw1on  7182  indpi  7283  nnindnn  7834  sup3exmid  8852  nnssre  8861  nnind  8873  nnsub  8896  dfuzi  9301  indstr  9531  cnref1o  9588  frec2uzsucd  10336  uzsinds  10377  ser0f  10450  bccl  10680  rexuz3  10932  isumlessdc  11437  prodf1f  11484  iprodap0  11523  eff2  11621  reeff1  11641  prmind2  12052  3prm  12060  sqrt2irr  12094  phisum  12172  pockthi  12288  1arith  12297  1arith2  12298  prminf  12388  isbasis3g  12684  distop  12725  cdivcncfap  13227  dveflem  13327  ioocosf1o  13415  2irrexpqap  13536  2sqlem6  13596  2sqlem10  13601  bj-indint  13813  bj-nnelirr  13835  bj-omord  13842  012of  13875  2o01f  13876  0nninf  13884  nconstwlpolem0  13941