Theorem rgen2w 3153

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

Syntax hints:  ∀wral 3140

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

This theorem depends on definitions:  df-bi 209  df-ral 3145

This theorem is referenced by:  porpss  7455  fnmpoi  7770  relmpoopab  7791  cantnfvalf  9130  ixxf  12751  fzf  12899  fzof  13038  rexfiuz  14709  sadcf  15804  prdsval  16730  prdsds  16739  homfeq  16966  comfeq  16978  wunnat  17228  eldmcoa  17327  catcfuccl  17371  relxpchom  17433  catcxpccl  17459  plusffval  17860  grpsubfval  18149  lsmass  18797  efgval2  18852  dmdprd  19122  dprdval  19127  scaffval  19654  ipffval  20794  eltx  22178  xkotf  22195  txcnp  22230  txcnmpt  22234  txrest  22241  txlm  22258  txflf  22616  dscmet  23184  xrtgioo  23416  ishtpy  23578  opnmblALT  24206  tglnfn  26335  wwlksonvtx  27635  wspthnonp  27639  clwwlknondisj  27892  hlimreui  29018  aciunf1lem  30409  ofoprabco  30411  dya2iocct  31540  icoreresf  34635  curfv  34874  ptrest  34893  poimirlem26  34920  rrnval  35107  atpsubN  36891  clsk3nimkb  40397