Theorem rgen2w 2819

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

Syntax hints:  A.wral 2807

This theorem is referenced by:  porpss  6584  fnmpt2i  6869  relmpt2opab  6882  cantnfvalf  8105  ixxf  11568  fzf  11705  fzof  11826  rexfiuz  13180  sadcf  14103  prdsval  14852  prdsds  14861  homfeq  15089  comfeq  15101  wunnat  15325  eldmcoa  15392  catcfuccl  15436  relxpchom  15450  catcxpccl  15476  plusffval  15877  lsmass  16688  efgval2  16742  dmdprd  17029  dprdval  17034  dprdvalOLD  17036  scaffval  17530  ipffval  18683  eltx  20069  xkotf  20086  txcnp  20121  txcnmpt  20125  txrest  20132  txlm  20149  txflf  20507  dscmet  21093  xrtgioo  21311  ishtpy  21472  opnmblALT  22012  tglnfn  23934  numclwwlkdisj  25080  hlimreui  26157  ofoprabco  27505  dya2iocct  28251  sseqfv2  28333  ptrest  30048  rrnval  30323  atpsubN  35477

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

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