Theorem rgen2w 2925

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

Hypothesis

Ref	Expression
rgenw.1	|- ph

Assertion

Ref	Expression
rgen2w	|- A. x e. A A. y e. B ph

Proof of Theorem rgen2w

Step	Hyp	Ref	Expression
1		rgenw.1	. . 3 |- ph
2	1	rgenw 2924	. 2 |- A. y e. B ph
3	2	rgenw 2924	1 |- A. x e. A A. y e. B ph

Syntax hints:   A.wral 2912

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

This theorem depends on definitions:  df-bi 197  df-ral 2917

This theorem is referenced by:  porpss  6941  fnmpt2i  7239  relmpt2opab  7259  cantnfvalf  8562  ixxf  12185  fzf  12330  fzof  12467  rexfiuz  14087  sadcf  15175  prdsval  16115  prdsds  16124  homfeq  16354  comfeq  16366  wunnat  16616  eldmcoa  16715  catcfuccl  16759  relxpchom  16821  catcxpccl  16847  plusffval  17247  lsmass  18083  efgval2  18137  dmdprd  18397  dprdval  18402  scaffval  18881  ipffval  19993  eltx  21371  xkotf  21388  txcnp  21423  txcnmpt  21427  txrest  21434  txlm  21451  txflf  21810  dscmet  22377  xrtgioo  22609  ishtpy  22771  opnmblALT  23371  tglnfn  25442  wspthnonp  26744  clwwlksndisj  26973  hlimreui  28096  aciunf1lem  29462  ofoprabco  29464  dya2iocct  30342  icoreresf  33200  curfv  33389  ptrest  33408  poimirlem26  33435  rrnval  33626  atpsubN  35039  clsk3nimkb  38338