Theorem rgen 2530

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

Syntax hints:   → wi 4   ∈ wcel 2148  ∀wral 2455

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 1449

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

This theorem is referenced by:  rgen2a  2531  rgenw  2532  mprg  2534  mprgbir  2535  rgen2  2563  r19.21be  2568  nrex  2569  rexlimi  2587  sbcth2  3050  reuss  3416  ral0  3524  unimax  3843  mpteq1  4087  mpteq2ia  4089  ordon  4485  tfis  4582  finds  4599  finds2  4600  ordom  4606  omsinds  4621  dmxpid  4848  fnopab  5340  fmpti  5668  opabex3  6122  oawordriexmid  6470  fifo  6978  inresflem  7058  0ct  7105  infnninf  7121  infnninfOLD  7122  exmidonfinlem  7191  pw1on  7224  netap  7252  2omotaplemap  7255  indpi  7340  nnindnn  7891  aptap  8606  sup3exmid  8913  nnssre  8922  nnind  8934  nnsub  8957  dfuzi  9362  indstr  9592  cnref1o  9649  frec2uzsucd  10400  uzsinds  10441  ser0f  10514  bccl  10746  rexuz3  10998  isumlessdc  11503  prodf1f  11550  iprodap0  11589  eff2  11687  reeff1  11707  prmind2  12119  3prm  12127  sqrt2irr  12161  phisum  12239  pockthi  12355  1arith  12364  1arith2  12365  prminf  12455  xpsff1o  12767  mgpf  13192  cnfld1  13436  cnsubglem  13443  isbasis3g  13516  distop  13555  cdivcncfap  14057  dveflem  14157  ioocosf1o  14245  2irrexpqap  14366  2sqlem6  14437  2sqlem10  14442  bj-indint  14653  bj-nnelirr  14675  bj-omord  14682  012of  14715  2o01f  14716  0nninf  14723  nconstwlpolem0  14780