Theorem rgen2w 3057

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

Syntax hints:  ∀wral 3052

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

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

This theorem is referenced by:  porpss  7674  fnmpoi  8016  mptmpoopabbrd  8026  relmpoopab  8037  cantnfvalf  9577  ixxf  13299  fzf  13456  fzof  13601  rexfiuz  15301  sadcf  16413  prdsvallem  17408  prdsds  17418  homfeq  17651  comfeq  17663  wunnat  17917  eldmcoa  18023  catcfuccl  18076  relxpchom  18138  catcxpccl  18164  plusffval  18605  grpsubfval  18950  lsmass  19635  efgval2  19690  dmdprd  19966  dprdval  19971  scaffval  20866  ipffval  21638  psdmul  22142  eltx  23543  xkotf  23560  txcnp  23595  txcnmpt  23599  txrest  23606  txlm  23623  txflf  23981  dscmet  24547  xrtgioo  24782  ishtpy  24949  opnmblALT  25580  zsoring  28415  tglnfn  28629  wwlksonvtx  29938  wspthnonp  29942  clwwlknondisj  30196  hlimreui  31325  aciunf1lem  32750  ofoprabco  32752  lsmssass  33477  dya2iocct  34440  mh-inf3sn  36740  icoreresf  37682  curfv  37935  ptrest  37954  poimirlem26  37981  rrnval  38162  disjimeceqbi  39141  atpsubN  40213  clsk3nimkb  44485  2arymaptf1  49141