Theorem rgen2w 3060

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

Syntax hints:  ∀wral 3055

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 209  df-ral 3056

This theorem is referenced by:  porpss  7674  fnmpoi  8016  mptmpoopabbrd  8026  relmpoopab  8037  cantnfvalf  9581  ixxf  13303  fzf  13460  fzof  13605  rexfiuz  15305  sadcf  16417  prdsvallem  17412  prdsds  17422  homfeq  17655  comfeq  17667  wunnat  17921  eldmcoa  18027  catcfuccl  18080  relxpchom  18142  catcxpccl  18168  plusffval  18609  grpsubfval  18954  lsmass  19639  efgval2  19694  dmdprd  19970  dprdval  19975  scaffval  20874  ipffval  21627  psdmul  22158  eltx  23555  xkotf  23572  txcnp  23607  txcnmpt  23611  txrest  23618  txlm  23635  txflf  23993  dscmet  24559  xrtgioo  24794  ishtpy  24961  opnmblALT  25592  zsoring  28423  tglnfn  28637  wwlksonvtx  29945  wspthnonp  29949  clwwlknondisj  30203  hlimreui  31332  aciunf1lem  32758  ofoprabco  32760  lsmssass  33489  dya2iocct  34476  mh-inf3sn  36785  icoreresf  37729  curfv  37982  ptrest  38001  poimirlem26  38028  rrnval  38209  disjimeceqbi  39188  atpsubN  40260  clsk3nimkb  44499  2arymaptf1  49158