Theorem rgen2w 2909

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 2908	. 2 ⊢ ∀𝑦 ∈ 𝐵 𝜑
3	2	rgenw 2908	1 ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑

Syntax hints:  ∀wral 2896

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

This theorem depends on definitions:  df-bi 196  df-ral 2901

This theorem is referenced by:  porpss  6839  fnmpt2i  7128  relmpt2opab  7146  cantnfvalf  8445  ixxf  12056  fzf  12201  fzof  12336  rexfiuz  13935  sadcf  15013  prdsval  15938  prdsds  15947  homfeq  16177  comfeq  16189  wunnat  16439  eldmcoa  16538  catcfuccl  16582  relxpchom  16644  catcxpccl  16670  plusffval  17070  lsmass  17906  efgval2  17960  dmdprd  18220  dprdval  18225  scaffval  18704  ipffval  19812  eltx  21181  xkotf  21198  txcnp  21233  txcnmpt  21237  txrest  21244  txlm  21261  txflf  21620  dscmet  22187  xrtgioo  22417  ishtpy  22579  opnmblALT  23177  tglnfn  25242  numclwwlkdisj  26607  hlimreui  27480  aciunf1lem  28844  ofoprabco  28847  dya2iocct  29669  sseqfv2  29783  icoreresf  32376  curfv  32559  ptrest  32578  poimirlem26  32605  rrnval  32796  atpsubN  34057  clsk3nimkb  37358  wspthnonp  41055  clwwlksndisj  41280