Theorem rgen 2428

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

Syntax hints:   → wi 4   ∈ wcel 1438  ∀wral 2359

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1383

This theorem depends on definitions:  df-bi 115  df-ral 2364

This theorem is referenced by:  rgen2a  2429  rgenw  2430  mprg  2432  mprgbir  2433  rgen2  2459  r19.21be  2464  nrex  2465  rexlimi  2482  sbcth2  2924  reuss  3278  ral0  3379  unimax  3682  mpteq1  3914  mpteq2ia  3916  ordon  4293  tfis  4388  finds  4405  finds2  4406  ordom  4411  omsinds  4425  fnopab  5124  fmpti  5435  opabex3  5875  oawordriexmid  6213  inresflem  6731  infnninf  6784  indpi  6880  nnindnn  7407  nnssre  8398  nnind  8410  nnsub  8432  dfuzi  8826  indstr  9050  cnref1o  9102  frec2uzsucd  9773  uzsinds  9813  iser0f  9913  ser0f  9915  bccl  10140  rexuz3  10388  prmind2  11184  3prm  11192  sqrt2irr  11223  bj-indint  11472  bj-nnelirr  11494  bj-omord  11501  0nninf  11539