Theorem rgen 2560

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

Syntax hints:   → wi 4   ∈ wcel 2177  ∀wral 2485

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 1473

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

This theorem is referenced by:  rgen2a  2561  rgenw  2562  mprg  2564  mprgbir  2565  rgen2  2593  r19.21be  2598  nrex  2599  rexlimi  2617  sbcth2  3090  reuss  3458  ral0  3566  unimax  3889  mpteq1  4135  mpteq2ia  4137  ordon  4541  tfis  4638  finds  4655  finds2  4656  ordom  4662  omsinds  4677  dmxpid  4907  fnopab  5409  fmpti  5744  opabex3  6219  oawordriexmid  6568  fifo  7096  inresflem  7176  0ct  7223  infnninf  7240  infnninfOLD  7241  exmidonfinlem  7316  pw1on  7353  netap  7381  2omotaplemap  7384  indpi  7470  nnindnn  8021  aptap  8738  sup3exmid  9045  nnssre  9055  nnind  9067  nnsub  9090  dfuzi  9498  indstr  9729  cnref1o  9787  frec2uzsucd  10563  uzsinds  10606  ser0f  10696  bccl  10929  wrdind  11193  rexuz3  11371  isumlessdc  11877  prodf1f  11924  iprodap0  11963  eff2  12061  reeff1  12081  prmind2  12512  3prm  12520  sqrt2irr  12554  phisum  12633  pockthi  12751  1arith  12760  1arith2  12761  prminf  12896  xpsff1o  13251  rngmgpf  13769  mgpf  13843  cnfld1  14404  cnsubglem  14411  isbasis3g  14588  distop  14627  cdivcncfap  15146  dveflem  15268  ioocosf1o  15396  2irrexpqap  15520  2sqlem6  15667  2sqlem10  15672  bj-indint  16001  bj-nnelirr  16023  bj-omord  16030  012of  16065  2o01f  16066  0nninf  16076  nconstwlpolem0  16137