Theorem rgen2w 3066

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

Syntax hints:  ∀wral 3061

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 206  df-ral 3062

This theorem is referenced by:  porpss  7716  fnmpoi  8055  relmpoopab  8079  cantnfvalf  9659  ixxf  13333  fzf  13487  fzof  13628  rexfiuz  15293  sadcf  16393  prdsvallem  17399  prdsds  17409  homfeq  17637  comfeq  17649  wunnat  17906  wunnatOLD  17907  eldmcoa  18014  catcfuccl  18068  catcfucclOLD  18069  relxpchom  18132  catcxpccl  18158  catcxpcclOLD  18159  plusffval  18566  grpsubfval  18867  lsmass  19536  efgval2  19591  dmdprd  19867  dprdval  19872  scaffval  20489  ipffval  21200  eltx  23071  xkotf  23088  txcnp  23123  txcnmpt  23127  txrest  23134  txlm  23151  txflf  23509  dscmet  24080  xrtgioo  24321  ishtpy  24487  opnmblALT  25119  tglnfn  27795  wwlksonvtx  29106  wspthnonp  29110  clwwlknondisj  29361  hlimreui  30487  aciunf1lem  31882  ofoprabco  31884  lsmssass  32507  dya2iocct  33274  icoreresf  36228  curfv  36463  ptrest  36482  poimirlem26  36509  rrnval  36690  atpsubN  38619  clsk3nimkb  42781  2arymaptf1  47329