Theorem rgen2w 3056

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

Syntax hints:  ∀wral 3051

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 3052

This theorem is referenced by:  porpss  7681  fnmpoi  8023  mptmpoopabbrd  8033  relmpoopab  8044  cantnfvalf  9586  ixxf  13308  fzf  13465  fzof  13610  rexfiuz  15310  sadcf  16422  prdsvallem  17417  prdsds  17427  homfeq  17660  comfeq  17672  wunnat  17926  eldmcoa  18032  catcfuccl  18085  relxpchom  18147  catcxpccl  18173  plusffval  18614  grpsubfval  18959  lsmass  19644  efgval2  19699  dmdprd  19975  dprdval  19980  scaffval  20875  ipffval  21628  psdmul  22132  eltx  23533  xkotf  23550  txcnp  23585  txcnmpt  23589  txrest  23596  txlm  23613  txflf  23971  dscmet  24537  xrtgioo  24772  ishtpy  24939  opnmblALT  25570  zsoring  28401  tglnfn  28615  wwlksonvtx  29923  wspthnonp  29927  clwwlknondisj  30181  hlimreui  31310  aciunf1lem  32735  ofoprabco  32737  lsmssass  33462  dya2iocct  34424  mh-inf3sn  36724  icoreresf  37668  curfv  37921  ptrest  37940  poimirlem26  37967  rrnval  38148  disjimeceqbi  39127  atpsubN  40199  clsk3nimkb  44467  2arymaptf1  49129