Theorem rgen2w 2954

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

Syntax hints:  ∀wral 2941

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

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

This theorem is referenced by:  porpss  6983  fnmpt2i  7284  relmpt2opab  7304  cantnfvalf  8600  ixxf  12223  fzf  12368  fzof  12506  rexfiuz  14131  sadcf  15222  prdsval  16162  prdsds  16171  homfeq  16401  comfeq  16413  wunnat  16663  eldmcoa  16762  catcfuccl  16806  relxpchom  16868  catcxpccl  16894  plusffval  17294  lsmass  18129  efgval2  18183  dmdprd  18443  dprdval  18448  scaffval  18929  ipffval  20041  eltx  21419  xkotf  21436  txcnp  21471  txcnmpt  21475  txrest  21482  txlm  21499  txflf  21857  dscmet  22424  xrtgioo  22656  ishtpy  22818  opnmblALT  23417  tglnfn  25487  wwlksonvtx  26805  wspthnonp  26813  clwwlknondisj  27086  clwwlknondisjOLD  27090  hlimreui  28224  aciunf1lem  29590  ofoprabco  29592  dya2iocct  30470  icoreresf  33330  curfv  33519  ptrest  33538  poimirlem26  33565  rrnval  33756  atpsubN  35357  clsk3nimkb  38655