Theorem rgen 2547

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

Syntax hints:   → wi 4   ∈ wcel 2164  ∀wral 2472

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 1460

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

This theorem is referenced by:  rgen2a  2548  rgenw  2549  mprg  2551  mprgbir  2552  rgen2  2580  r19.21be  2585  nrex  2586  rexlimi  2604  sbcth2  3074  reuss  3441  ral0  3549  unimax  3870  mpteq1  4114  mpteq2ia  4116  ordon  4519  tfis  4616  finds  4633  finds2  4634  ordom  4640  omsinds  4655  dmxpid  4884  fnopab  5379  fmpti  5711  opabex3  6176  oawordriexmid  6525  fifo  7041  inresflem  7121  0ct  7168  infnninf  7185  infnninfOLD  7186  exmidonfinlem  7255  pw1on  7288  netap  7316  2omotaplemap  7319  indpi  7404  nnindnn  7955  aptap  8671  sup3exmid  8978  nnssre  8988  nnind  9000  nnsub  9023  dfuzi  9430  indstr  9661  cnref1o  9719  frec2uzsucd  10475  uzsinds  10518  ser0f  10608  bccl  10841  rexuz3  11137  isumlessdc  11642  prodf1f  11689  iprodap0  11728  eff2  11826  reeff1  11846  prmind2  12261  3prm  12269  sqrt2irr  12303  phisum  12381  pockthi  12499  1arith  12508  1arith2  12509  prminf  12615  xpsff1o  12935  rngmgpf  13436  mgpf  13510  cnfld1  14071  cnsubglem  14078  isbasis3g  14225  distop  14264  cdivcncfap  14783  dveflem  14905  ioocosf1o  15030  2irrexpqap  15151  2sqlem6  15277  2sqlem10  15282  bj-indint  15493  bj-nnelirr  15515  bj-omord  15522  012of  15556  2o01f  15557  0nninf  15564  nconstwlpolem0  15623