Theorem rgen2w 3067

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

Syntax hints:  ∀wral 3062

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

This theorem depends on definitions:  df-bi 206  df-ral 3063

This theorem is referenced by:  porpss  7717  fnmpoi  8056  relmpoopab  8080  cantnfvalf  9660  ixxf  13334  fzf  13488  fzof  13629  rexfiuz  15294  sadcf  16394  prdsvallem  17400  prdsds  17410  homfeq  17638  comfeq  17650  wunnat  17907  wunnatOLD  17908  eldmcoa  18015  catcfuccl  18069  catcfucclOLD  18070  relxpchom  18133  catcxpccl  18159  catcxpcclOLD  18160  plusffval  18567  grpsubfval  18868  lsmass  19537  efgval2  19592  dmdprd  19868  dprdval  19873  scaffval  20490  ipffval  21201  eltx  23072  xkotf  23089  txcnp  23124  txcnmpt  23128  txrest  23135  txlm  23152  txflf  23510  dscmet  24081  xrtgioo  24322  ishtpy  24488  opnmblALT  25120  tglnfn  27829  wwlksonvtx  29140  wspthnonp  29144  clwwlknondisj  29395  hlimreui  30523  aciunf1lem  31918  ofoprabco  31920  lsmssass  32543  dya2iocct  33310  icoreresf  36281  curfv  36516  ptrest  36535  poimirlem26  36562  rrnval  36743  atpsubN  38672  clsk3nimkb  42839  2arymaptf1  47387