Theorem rgen2w 3065

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

Syntax hints:  ∀wral 3060

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 3061

This theorem is referenced by:  porpss  7700  fnmpoi  8038  relmpoopab  8062  cantnfvalf  9642  ixxf  13316  fzf  13470  fzof  13611  rexfiuz  15276  sadcf  16376  prdsvallem  17382  prdsds  17392  homfeq  17620  comfeq  17632  wunnat  17889  wunnatOLD  17890  eldmcoa  17997  catcfuccl  18051  catcfucclOLD  18052  relxpchom  18115  catcxpccl  18141  catcxpcclOLD  18142  plusffval  18549  grpsubfval  18843  lsmass  19501  efgval2  19556  dmdprd  19827  dprdval  19832  scaffval  20439  ipffval  21134  eltx  23001  xkotf  23018  txcnp  23053  txcnmpt  23057  txrest  23064  txlm  23081  txflf  23439  dscmet  24010  xrtgioo  24251  ishtpy  24417  opnmblALT  25049  tglnfn  27663  wwlksonvtx  28974  wspthnonp  28978  clwwlknondisj  29229  hlimreui  30355  aciunf1lem  31756  ofoprabco  31758  lsmssass  32370  dya2iocct  33110  icoreresf  36037  curfv  36272  ptrest  36291  poimirlem26  36318  rrnval  36500  atpsubN  38429  clsk3nimkb  42562  2arymaptf1  46987