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  7401  0ct  7448  infnninf  7465  infnninfOLD  7466  exmidonfinlem  7546  pw1on  7586  netap  7621  2omotaplemap  7624  indpi  7710  nnindnn  8261  aptap  8981  sup3exmid  9290  nnssre  9311  nnind  9323  nnsub  9346  dfuzi  9761  indstr  10003  cnref1o  10062  frec2uzsucd  10852  uzsinds  10895  ser0f  10985  bccl  11220  hashfibc  11298  wrdind  11509  rexuz3  11771  isumlessdc  12281  prodf1f  12328  iprodap0  12367  eff2  12465  reeff1  12485  prmind2  12916  3prm  12924  sqrt2irr  12959  phisum  13041  pockthi  13159  1arith  13168  1arith2  13169  prmlem1a  13243  ballotfilemofi  13270  ballotfilem2  13279  ballotfilemefi  13288  ballotfilemafi  13289  ballotfilembfi  13290  ballotfilem7  13330  prminf  13397  xpsff1o  13721  rngmgpf  14287  mgpf  14366  cnfld1  14960  cnsubglem  14967  isbasis3g  15199  distop  15238  cdivcncfap  15757  dveflem  15879  ioocosf1o  16008  2irrexpqap  16136  chtqub  16218  2sqlem6  16361  2sqlem10  16366  konigsberglem5  16855  bj-indint  17079  bj-nnelirr  17101  bj-omord  17108  012of  17145  2o01f  17146  0nninf  17169  nconstwlpolem0  17235