Theorem rgen2w 3074

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 3073	. 2 ⊢ ∀𝑦 ∈ 𝐵 𝜑
3	2	rgenw 3073	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 1803

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

This theorem is referenced by:  porpss  7515  fnmpoi  7840  relmpoopab  7862  cantnfvalf  9280  ixxf  12945  fzf  13099  fzof  13240  rexfiuz  14911  sadcf  16012  prdsvallem  16959  prdsds  16969  homfeq  17197  comfeq  17209  wunnat  17463  wunnatOLD  17464  eldmcoa  17571  catcfuccl  17625  catcfucclOLD  17626  relxpchom  17688  catcxpccl  17714  catcxpcclOLD  17715  plusffval  18120  grpsubfval  18411  lsmass  19059  efgval2  19114  dmdprd  19385  dprdval  19390  scaffval  19917  ipffval  20610  eltx  22465  xkotf  22482  txcnp  22517  txcnmpt  22521  txrest  22528  txlm  22545  txflf  22903  dscmet  23470  xrtgioo  23703  ishtpy  23869  opnmblALT  24500  tglnfn  26638  wwlksonvtx  27939  wspthnonp  27943  clwwlknondisj  28194  hlimreui  29320  aciunf1lem  30719  ofoprabco  30721  lsmssass  31304  dya2iocct  31959  icoreresf  35260  curfv  35494  ptrest  35513  poimirlem26  35540  rrnval  35722  atpsubN  37504  clsk3nimkb  41327  2arymaptf1  45672