Theorem rgen 2550

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

Syntax hints:   → wi 4   ∈ wcel 2167  ∀wral 2475

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 1463

This theorem depends on definitions:  df-bi 117  df-ral 2480

This theorem is referenced by:  rgen2a  2551  rgenw  2552  mprg  2554  mprgbir  2555  rgen2  2583  r19.21be  2588  nrex  2589  rexlimi  2607  sbcth2  3077  reuss  3445  ral0  3553  unimax  3874  mpteq1  4118  mpteq2ia  4120  ordon  4523  tfis  4620  finds  4637  finds2  4638  ordom  4644  omsinds  4659  dmxpid  4888  fnopab  5385  fmpti  5717  opabex3  6188  oawordriexmid  6537  fifo  7055  inresflem  7135  0ct  7182  infnninf  7199  infnninfOLD  7200  exmidonfinlem  7274  pw1on  7311  netap  7339  2omotaplemap  7342  indpi  7428  nnindnn  7979  aptap  8696  sup3exmid  9003  nnssre  9013  nnind  9025  nnsub  9048  dfuzi  9455  indstr  9686  cnref1o  9744  frec2uzsucd  10512  uzsinds  10555  ser0f  10645  bccl  10878  rexuz3  11174  isumlessdc  11680  prodf1f  11727  iprodap0  11766  eff2  11864  reeff1  11884  prmind2  12315  3prm  12323  sqrt2irr  12357  phisum  12436  pockthi  12554  1arith  12563  1arith2  12564  prminf  12699  xpsff1o  13053  rngmgpf  13571  mgpf  13645  cnfld1  14206  cnsubglem  14213  isbasis3g  14368  distop  14407  cdivcncfap  14926  dveflem  15048  ioocosf1o  15176  2irrexpqap  15300  2sqlem6  15447  2sqlem10  15452  bj-indint  15663  bj-nnelirr  15685  bj-omord  15692  012of  15726  2o01f  15727  0nninf  15737  nconstwlpolem0  15798