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  4216  mpteq2ia  4219  ordon  4635  tfis  4732  finds  4749  finds2  4750  ordom  4756  omsinds  4771  dmxpid  5005  fnopab  5511  fmpti  5863  opabex3  6355  oawordriexmid  6747  fifo  7320  inresflem  7407  0ct  7454  infnninf  7471  infnninfOLD  7472  exmidonfinlem  7552  pw1on  7592  netap  7627  2omotaplemap  7630  indpi  7716  nnindnn  8267  aptap  8987  sup3exmid  9296  nnssre  9318  nnind  9330  nnsub  9353  dfuzi  9768  indstr  10010  cnref1o  10069  frec2uzsucd  10860  uzsinds  10903  ser0f  10993  bccl  11228  hashfibc  11306  wrdind  11517  rexuz3  11779  isumlessdc  12289  prodf1f  12336  iprodap0  12375  eff2  12473  reeff1  12493  prmind2  12924  3prm  12932  sqrt2irr  12967  phisum  13049  pockthi  13167  1arith  13176  1arith2  13177  prmlem1a  13251  ballotfilemofi  13278  ballotfilem2  13287  ballotfilemefi  13296  ballotfilemafi  13297  ballotfilembfi  13298  ballotfilem7  13338  prminf  13405  xpsff1o  13730  rngmgpf  14344  mgpf  14423  cnfld1  15019  cnsubglem  15026  isbasis3g  15284  distop  15323  cdivcncfap  15842  dveflem  15964  ioocosf1o  16094  2irrexpqap  16226  chtqub  16308  2sqlem6  16456  2sqlem10  16461  konigsberglem5  16950  bj-indint  17174  bj-nnelirr  17196  bj-omord  17203  012of  17240  2o01f  17241  0nninf  17265  nconstwlpolem0  17332