Theorem rgen 1247

Description: Generalization rule for restricted quantification.

Hypothesis

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

Assertion

Ref	Expression
rgen	⊢ ∀x ∈ A φ

Proof of Theorem rgen

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

Syntax hints:   → wi 2   ∈ wcel 1092  ∀wral 1201

This theorem is referenced by:  rgen2 1248  mprg 1249  mprgbir 1250  rgen2a 1264  r19.21be 1269  nrex 1270  unisseq 1946  tfis 2245  onssmin 2263  finds 2397  finds2 2399  fnopab 2746  canth 2945  pw2en 3348  nneneq 3408  dfom3 3477  rankval3 3525  rankuni 3533  rankun 3535  scottex 3541  cplem1 3545  aceq5lem4 3561  kmlem1 3580  cardiun 3665  cflem 3700  cflecard 3707  cfsuc 3709  dmrecpq 3868  1pr 3911  reclem2pr 3951  nnleltp1t 4448  indstr 4611  sqrlem6 4736  sqrlem13 4743  sqr2irrlem3 4779  clim0 4882  ruclem33 4917  ruclem35 4919  normlem6 5068  hlim0 5140  hlimcaui 5141  shsspwh 5153  projlem8 5200  projlem13 5205  hosf 5602  hodf 5603  hoscom 5605  hosass 5607  hosdir 5609  hoddir 5610  ho0 5612  ho1 5613  hoid0 5614  hoid1 5617  hoid1r 5618  pjsdi 5625  pjddi 5626  pjtot 5644

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-gen 677

This theorem depends on definitions:  df-bi 128  df-ral 1205

metamath.org