Theorem rgen2w 3101

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

Syntax hints:  ∀wral 3088

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

This theorem depends on definitions:  df-bi 199  df-ral 3093

This theorem is referenced by:  porpss  7273  fnmpoi  7578  relmpoopab  7599  cantnfvalf  8924  ixxf  12567  fzf  12715  fzof  12854  rexfiuz  14571  sadcf  15665  prdsval  16587  prdsds  16596  homfeq  16825  comfeq  16837  wunnat  17087  eldmcoa  17186  catcfuccl  17230  relxpchom  17292  catcxpccl  17318  plusffval  17718  grpsubfval  17937  lsmass  18557  efgval2  18611  dmdprd  18873  dprdval  18878  scaffval  19377  ipffval  20497  eltx  21883  xkotf  21900  txcnp  21935  txcnmpt  21939  txrest  21946  txlm  21963  txflf  22321  dscmet  22888  xrtgioo  23120  ishtpy  23282  opnmblALT  23910  tglnfn  26038  wwlksonvtx  27344  wspthnonp  27348  clwwlknondisj  27642  hlimreui  28798  aciunf1lem  30172  ofoprabco  30174  dya2iocct  31183  icoreresf  34075  curfv  34313  ptrest  34332  poimirlem26  34359  rrnval  34547  atpsubN  36334  clsk3nimkb  39753