Theorem rgen 2523

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

Syntax hints:   → wi 4   ∈ wcel 2141  ∀wral 2448

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

This theorem depends on definitions:  df-bi 116  df-ral 2453

This theorem is referenced by:  rgen2a  2524  rgenw  2525  mprg  2527  mprgbir  2528  rgen2  2556  r19.21be  2561  nrex  2562  rexlimi  2580  sbcth2  3042  reuss  3408  ral0  3515  unimax  3828  mpteq1  4071  mpteq2ia  4073  ordon  4468  tfis  4565  finds  4582  finds2  4583  ordom  4589  omsinds  4604  dmxpid  4830  fnopab  5320  fmpti  5646  opabex3  6099  oawordriexmid  6447  fifo  6954  inresflem  7034  0ct  7081  infnninf  7097  infnninfOLD  7098  exmidonfinlem  7159  pw1on  7192  indpi  7293  nnindnn  7844  sup3exmid  8862  nnssre  8871  nnind  8883  nnsub  8906  dfuzi  9311  indstr  9541  cnref1o  9598  frec2uzsucd  10346  uzsinds  10387  ser0f  10460  bccl  10690  rexuz3  10943  isumlessdc  11448  prodf1f  11495  iprodap0  11534  eff2  11632  reeff1  11652  prmind2  12063  3prm  12071  sqrt2irr  12105  phisum  12183  pockthi  12299  1arith  12308  1arith2  12309  prminf  12399  isbasis3g  12799  distop  12840  cdivcncfap  13342  dveflem  13442  ioocosf1o  13530  2irrexpqap  13651  2sqlem6  13711  2sqlem10  13716  bj-indint  13928  bj-nnelirr  13950  bj-omord  13957  012of  13990  2o01f  13991  0nninf  13999  nconstwlpolem0  14056