Theorem rgen2w 3057

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

Syntax hints:  ∀wral 3052

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

This theorem depends on definitions:  df-bi 207  df-ral 3053

This theorem is referenced by:  porpss  7684  fnmpoi  8026  mptmpoopabbrd  8036  relmpoopab  8048  cantnfvalf  9588  ixxf  13285  fzf  13441  fzof  13586  rexfiuz  15285  sadcf  16394  prdsvallem  17388  prdsds  17398  homfeq  17631  comfeq  17643  wunnat  17897  eldmcoa  18003  catcfuccl  18056  relxpchom  18118  catcxpccl  18144  plusffval  18585  grpsubfval  18930  lsmass  19615  efgval2  19670  dmdprd  19946  dprdval  19951  scaffval  20848  ipffval  21620  psdmul  22126  eltx  23529  xkotf  23546  txcnp  23581  txcnmpt  23585  txrest  23592  txlm  23609  txflf  23967  dscmet  24533  xrtgioo  24768  ishtpy  24944  opnmblALT  25577  zsoring  28422  tglnfn  28637  wwlksonvtx  29946  wspthnonp  29950  clwwlknondisj  30204  hlimreui  31333  aciunf1lem  32758  ofoprabco  32760  lsmssass  33501  dya2iocct  34464  icoreresf  37634  curfv  37880  ptrest  37899  poimirlem26  37926  rrnval  38107  disjimeceqbi  39086  atpsubN  40158  clsk3nimkb  44425  2arymaptf1  49042