Theorem rgen 2583

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

Syntax hints:   → wi 4   ∈ wcel 2200  ∀wral 2508

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

This theorem depends on definitions:  df-bi 117  df-ral 2513

This theorem is referenced by:  rgen2a  2584  rgenw  2585  mprg  2587  mprgbir  2588  rgen2  2616  r19.21be  2621  nrex  2622  rexlimi  2641  sbcth2  3117  reuss  3485  ral0  3593  unimax  3922  mpteq1  4168  mpteq2ia  4170  ordon  4579  tfis  4676  finds  4693  finds2  4694  ordom  4700  omsinds  4715  dmxpid  4948  fnopab  5451  fmpti  5792  opabex3  6276  oawordriexmid  6629  fifo  7163  inresflem  7243  0ct  7290  infnninf  7307  infnninfOLD  7308  exmidonfinlem  7387  pw1on  7427  netap  7456  2omotaplemap  7459  indpi  7545  nnindnn  8096  aptap  8813  sup3exmid  9120  nnssre  9130  nnind  9142  nnsub  9165  dfuzi  9573  indstr  9805  cnref1o  9863  frec2uzsucd  10640  uzsinds  10683  ser0f  10773  bccl  11006  wrdind  11275  rexuz3  11522  isumlessdc  12028  prodf1f  12075  iprodap0  12114  eff2  12212  reeff1  12232  prmind2  12663  3prm  12671  sqrt2irr  12705  phisum  12784  pockthi  12902  1arith  12911  1arith2  12912  prminf  13047  xpsff1o  13403  rngmgpf  13921  mgpf  13995  cnfld1  14557  cnsubglem  14564  isbasis3g  14741  distop  14780  cdivcncfap  15299  dveflem  15421  ioocosf1o  15549  2irrexpqap  15673  2sqlem6  15820  2sqlem10  15825  bj-indint  16403  bj-nnelirr  16425  bj-omord  16432  012of  16470  2o01f  16471  0nninf  16484  nconstwlpolem0  16545