Theorem rgen2w 3050

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

Syntax hints:  ∀wral 3045

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

This theorem depends on definitions:  df-bi 207  df-ral 3046

This theorem is referenced by:  porpss  7706  fnmpoi  8052  mptmpoopabbrd  8062  relmpoopab  8076  cantnfvalf  9625  ixxf  13323  fzf  13479  fzof  13624  rexfiuz  15321  sadcf  16430  prdsvallem  17424  prdsds  17434  homfeq  17662  comfeq  17674  wunnat  17928  eldmcoa  18034  catcfuccl  18087  relxpchom  18149  catcxpccl  18175  plusffval  18580  grpsubfval  18922  lsmass  19606  efgval2  19661  dmdprd  19937  dprdval  19942  scaffval  20793  ipffval  21564  psdmul  22060  eltx  23462  xkotf  23479  txcnp  23514  txcnmpt  23518  txrest  23525  txlm  23542  txflf  23900  dscmet  24467  xrtgioo  24702  ishtpy  24878  opnmblALT  25511  tglnfn  28481  wwlksonvtx  29792  wspthnonp  29796  clwwlknondisj  30047  hlimreui  31175  aciunf1lem  32593  ofoprabco  32595  lsmssass  33380  dya2iocct  34278  icoreresf  37347  curfv  37601  ptrest  37620  poimirlem26  37647  rrnval  37828  atpsubN  39754  clsk3nimkb  44036  2arymaptf1  48646