Theorem rgen2w 2763

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 2762	. 2
3	2	rgenw 2762	1

Syntax hints:  A.wral 2694

This theorem is referenced by:  porpss  6334  fnmpt2i  6612  relmpt2opab  6624  cantnfvalf  7820  ixxf  11255  fzf  11385  fzof  11491  rexfiuz  12776  sadcf  13589  prdsval  14333  prdsds  14342  homfeq  14573  comfeq  14585  wunnat  14806  eldmcoa  14873  catcfuccl  14917  relxpchom  14931  catcxpccl  14957  plusffval  15367  lsmass  16104  efgval2  16158  dmdprd  16368  dprdval  16370  scaffval  16779  ipffval  17785  eltx  18845  xkotf  18862  txcnp  18897  txcnmpt  18901  txrest  18908  txlm  18925  txflf  19283  dscmet  19865  xrtgioo  20083  ishtpy  20244  opnmblALT  20783  tglnfn  22718  hlimreui  24321  ofoprabco  25662  pstmxmet  26033  dya2iocct  26404  sseqfv2  26480  ptrest  28096  rrnval  28397  numclwwlkdisj  30347  atpsubN  32834

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

This theorem depends on definitions:  df-bi 179  df-ral 2699