Theorem rgen 2680

Description: Generalization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)

Hypothesis

Ref	Expression
rgen.1	⊢ (x ∈ A → φ)

Assertion

Ref	Expression
rgen	⊢ ∀x ∈ A φ

Proof of Theorem rgen

Step	Hyp	Ref	Expression
1		df-ral 2620	. 2 ⊢ (∀x ∈ A φ ↔ ∀x(x ∈ A → φ))
2		rgen.1	. 2 ⊢ (x ∈ A → φ)
3	1, 2	mpgbir 1550	1 ⊢ ∀x ∈ A φ

Syntax hints:   → wi 4   ∈ wcel 1710  ∀wral 2615

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546

This theorem depends on definitions:  df-bi 177  df-ral 2620

This theorem is referenced by:  rgen2a  2681  rgenw  2682  mprg  2684  mprgbir  2685  rgen2  2711  r19.21be  2716  nrex  2717  rexlimi  2732  sbcth2  3130  reuss  3537  r19.2zb  3641  ral0  3655  unimax  3926  nndisjeq  4430  fnopab  5208  mpteq1  5659  mpteq2ia  5660  fmpti  5694  clos1is  5882  nclenn  6250  nmembers1lem2  6270  nnc3n3p1  6279  nchoicelem12  6301