Theorem rgen 2530

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

Syntax hints:   → wi 4   ∈ wcel 2148  ∀wral 2455

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 1449

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

This theorem is referenced by:  rgen2a  2531  rgenw  2532  mprg  2534  mprgbir  2535  rgen2  2563  r19.21be  2568  nrex  2569  rexlimi  2587  sbcth2  3051  reuss  3417  ral0  3525  unimax  3844  mpteq1  4088  mpteq2ia  4090  ordon  4486  tfis  4583  finds  4600  finds2  4601  ordom  4607  omsinds  4622  dmxpid  4849  fnopab  5341  fmpti  5669  opabex3  6123  oawordriexmid  6471  fifo  6979  inresflem  7059  0ct  7106  infnninf  7122  infnninfOLD  7123  exmidonfinlem  7192  pw1on  7225  netap  7253  2omotaplemap  7256  indpi  7341  nnindnn  7892  aptap  8607  sup3exmid  8914  nnssre  8923  nnind  8935  nnsub  8958  dfuzi  9363  indstr  9593  cnref1o  9650  frec2uzsucd  10401  uzsinds  10442  ser0f  10515  bccl  10747  rexuz3  10999  isumlessdc  11504  prodf1f  11551  iprodap0  11590  eff2  11688  reeff1  11708  prmind2  12120  3prm  12128  sqrt2irr  12162  phisum  12240  pockthi  12356  1arith  12365  1arith2  12366  prminf  12456  xpsff1o  12768  mgpf  13194  cnfld1  13469  cnsubglem  13476  isbasis3g  13549  distop  13588  cdivcncfap  14090  dveflem  14190  ioocosf1o  14278  2irrexpqap  14399  2sqlem6  14470  2sqlem10  14475  bj-indint  14686  bj-nnelirr  14708  bj-omord  14715  012of  14748  2o01f  14749  0nninf  14756  nconstwlpolem0  14813