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 ⊢ ∀𝑥 ∈ 𝐴 𝜑

Syntax hints:   → wi 4   ∈ wcel 2209  ∀wral 2528

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 1502

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

This theorem is referenced 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  3967  mpteq1  4213  mpteq2ia  4215  ordon  4631  tfis  4728  finds  4745  finds2  4746  ordom  4752  omsinds  4767  dmxpid  5001  fnopab  5506  fmpti  5854  opabex3  6345  oawordriexmid  6737  fifo  7308  inresflem  7394  0ct  7441  infnninf  7458  infnninfOLD  7459  exmidonfinlem  7539  pw1on  7579  netap  7614  2omotaplemap  7617  indpi  7703  nnindnn  8254  aptap  8972  sup3exmid  9281  nnssre  9291  nnind  9303  nnsub  9326  dfuzi  9739  indstr  9976  cnref1o  10034  frec2uzsucd  10821  uzsinds  10864  ser0f  10954  bccl  11188  hashfibc  11266  wrdind  11477  rexuz3  11739  isumlessdc  12246  prodf1f  12293  iprodap0  12332  eff2  12430  reeff1  12450  prmind2  12881  3prm  12889  sqrt2irr  12923  phisum  13002  pockthi  13120  1arith  13129  1arith2  13130  ballotfilemofi  13202  ballotfilem2  13211  ballotfilemefi  13220  ballotfilemafi  13221  ballotfilembfi  13222  ballotfilem7  13262  prminf  13329  xpsff1o  13653  rngmgpf  14219  mgpf  14298  cnfld1  14892  cnsubglem  14899  isbasis3g  15130  distop  15169  cdivcncfap  15688  dveflem  15810  ioocosf1o  15938  2irrexpqap  16063  2sqlem6  16222  2sqlem10  16227  konigsberglem5  16716  bj-indint  16940  bj-nnelirr  16962  bj-omord  16969  012of  17006  2o01f  17007  0nninf  17021  nconstwlpolem0  17087