Theorem rgen 2603

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ∀wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1502

This proof depends on definitions:  df-bi 117  df-ral 2533

This theorem is used by:  rgen2a  2604  rgenw  2605  mprg  2607  mprgbir  2608  rgen2  2636  r19.21be  2641  nrex  2642  rexlimi  2661  sbcth2  3140  reuss  3514  ral0  3629  unimax  3969  mpteq1  4215  mpteq2ia  4217  ordon  4633  tfis  4730  finds  4747  finds2  4748  ordom  4754  omsinds  4769  dmxpid  5003  fnopab  5508  fmpti  5860  opabex3  6351  oawordriexmid  6743  fifo  7314  inresflem  7400  0ct  7447  infnninf  7464  infnninfOLD  7465  exmidonfinlem  7545  pw1on  7585  netap  7620  2omotaplemap  7623  indpi  7709  nnindnn  8260  aptap  8979  sup3exmid  9288  nnssre  9309  nnind  9321  nnsub  9344  dfuzi  9758  indstr  9995  cnref1o  10053  frec2uzsucd  10840  uzsinds  10883  ser0f  10973  bccl  11207  hashfibc  11285  wrdind  11496  rexuz3  11758  isumlessdc  12265  prodf1f  12312  iprodap0  12351  eff2  12449  reeff1  12469  prmind2  12900  3prm  12908  sqrt2irr  12942  phisum  13021  pockthi  13139  1arith  13148  1arith2  13149  ballotfilemofi  13221  ballotfilem2  13230  ballotfilemefi  13239  ballotfilemafi  13240  ballotfilembfi  13241  ballotfilem7  13281  prminf  13348  xpsff1o  13672  rngmgpf  14238  mgpf  14317  cnfld1  14911  cnsubglem  14918  isbasis3g  15149  distop  15188  cdivcncfap  15707  dveflem  15829  ioocosf1o  15958  2irrexpqap  16086  2sqlem6  16251  2sqlem10  16256  konigsberglem5  16745  bj-indint  16969  bj-nnelirr  16991  bj-omord  16998  012of  17035  2o01f  17036  0nninf  17059  nconstwlpolem0  17125