Theorem rgen2w 2904

Description: Generalization rule for restricted quantification. Note that and needn't be distinct. (Contributed by NM, 18-Jun-2014.)

Hypothesis

Ref	Expression
rgenw.1

Assertion

Ref	Expression
rgen2w

Proof of Theorem rgen2w

Step	Hyp	Ref	Expression
1		rgenw.1	. . 3
2	1	rgenw 2903	. 2
3	2	rgenw 2903	1

Syntax hints:  A.wral 2800

This theorem is referenced by:  porpss  6497  fnmpt2i  6776  relmpt2opab  6788  cantnfvalf  8010  ixxf  11449  fzf  11586  fzof  11695  rexfiuz  12993  sadcf  13807  prdsval  14552  prdsds  14561  homfeq  14792  comfeq  14804  wunnat  15025  eldmcoa  15092  catcfuccl  15136  relxpchom  15150  catcxpccl  15176  plusffval  15586  lsmass  16328  efgval2  16382  dmdprd  16655  dprdval  16660  dprdvalOLD  16662  scaffval  17142  ipffval  18270  eltx  19540  xkotf  19557  txcnp  19592  txcnmpt  19596  txrest  19603  txlm  19620  txflf  19978  dscmet  20564  xrtgioo  20782  ishtpy  20943  opnmblALT  21483  tglnfn  23398  hlimreui  25111  ofoprabco  26449  pstmxmet  26781  dya2iocct  27151  sseqfv2  27233  ptrest  28885  rrnval  29186  numclwwlkdisj  31550  atpsubN  34248

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592

This theorem depends on definitions:  df-bi 185  df-ral 2805