Theorem rgen2w 3090

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

Syntax hints:  ∀wral 3085

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

This theorem depends on definitions:  df-bi 210  df-ral 3086

This theorem is referenced by:  porpss  7725  fnmpoi  8067  mptmpoopabbrd  8078  relmpoopab  8089  cantnfvalf  9634  ixxf  13382  fzf  13539  fzof  13684  rexfiuz  15399  sadcf  16511  prdsvallem  17507  prdsds  17517  homfeq  17750  comfeq  17762  wunnat  18016  eldmcoa  18122  catcfuccl  18175  relxpchom  18237  catcxpccl  18263  plusffval  18704  grpsubfval  19050  lsmass  19739  efgval2  19794  dmdprd  20070  dprdval  20075  scaffval  20979  ipffval  21767  psdmul  22298  eltx  23694  xkotf  23711  txcnp  23746  txcnmpt  23750  txrest  23757  txlm  23774  txflf  24132  dscmet  24698  xrtgioo  24933  ishtpy  25100  opnmblALT  25731  zsoring  28568  tglnfn  28782  tgplnfn  29015  wwlksonvtx  30145  wspthnonp  30149  clwwlknondisj  30403  hlimreui  31532  aciunf1lem  32948  ofoprabco  32950  lsmssass  33655  dya2iocct  34615  vonf1osev  35529  mh-inf3sn  36976  icoreresf  37920  curfv  38173  ptrest  38192  poimirlem26  38219  rrnval  38400  disjimeceqbi  39379  atpsubN  40451  clsk3nimkb  44692  2arymaptf1  49352