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  27798  wwlksonvtx  29109  wspthnonp  29113  clwwlknondisj  29364  hlimreui  30492  aciunf1lem  31887  ofoprabco  31889  lsmssass  32512  dya2iocct  33279  icoreresf  36233  curfv  36468  ptrest  36487  poimirlem26  36514  rrnval  36695  atpsubN  38624  clsk3nimkb  42791  2arymaptf1  47339