Theorem rgen 2543

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

Syntax hints:   → wi 4   ∈ wcel 2160  ∀wral 2468

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 1460

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

This theorem is referenced by:  rgen2a  2544  rgenw  2545  mprg  2547  mprgbir  2548  rgen2  2576  r19.21be  2581  nrex  2582  rexlimi  2600  sbcth2  3065  reuss  3431  ral0  3539  unimax  3858  mpteq1  4102  mpteq2ia  4104  ordon  4503  tfis  4600  finds  4617  finds2  4618  ordom  4624  omsinds  4639  dmxpid  4866  fnopab  5359  fmpti  5688  opabex3  6146  oawordriexmid  6494  fifo  7008  inresflem  7088  0ct  7135  infnninf  7151  infnninfOLD  7152  exmidonfinlem  7221  pw1on  7254  netap  7282  2omotaplemap  7285  indpi  7370  nnindnn  7921  aptap  8636  sup3exmid  8943  nnssre  8952  nnind  8964  nnsub  8987  dfuzi  9392  indstr  9622  cnref1o  9679  frec2uzsucd  10431  uzsinds  10472  ser0f  10545  bccl  10778  rexuz3  11030  isumlessdc  11535  prodf1f  11582  iprodap0  11621  eff2  11719  reeff1  11739  prmind2  12151  3prm  12159  sqrt2irr  12193  phisum  12271  pockthi  12389  1arith  12398  1arith2  12399  prminf  12505  xpsff1o  12822  rngmgpf  13288  mgpf  13362  cnfld1  13872  cnsubglem  13879  isbasis3g  13998  distop  14037  cdivcncfap  14539  dveflem  14639  ioocosf1o  14727  2irrexpqap  14848  2sqlem6  14920  2sqlem10  14925  bj-indint  15136  bj-nnelirr  15158  bj-omord  15165  012of  15199  2o01f  15200  0nninf  15207  nconstwlpolem0  15265