Theorem rgen2w 3052

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

Syntax hints:  ∀wral 3047

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

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

This theorem is referenced by:  porpss  7660  fnmpoi  8002  mptmpoopabbrd  8012  relmpoopab  8024  cantnfvalf  9555  ixxf  13255  fzf  13411  fzof  13556  rexfiuz  15255  sadcf  16364  prdsvallem  17358  prdsds  17368  homfeq  17600  comfeq  17612  wunnat  17866  eldmcoa  17972  catcfuccl  18025  relxpchom  18087  catcxpccl  18113  plusffval  18554  grpsubfval  18896  lsmass  19581  efgval2  19636  dmdprd  19912  dprdval  19917  scaffval  20813  ipffval  21585  psdmul  22081  eltx  23483  xkotf  23500  txcnp  23535  txcnmpt  23539  txrest  23546  txlm  23563  txflf  23921  dscmet  24487  xrtgioo  24722  ishtpy  24898  opnmblALT  25531  zsoring  28332  tglnfn  28525  wwlksonvtx  29833  wspthnonp  29837  clwwlknondisj  30091  hlimreui  31219  aciunf1lem  32644  ofoprabco  32646  lsmssass  33367  dya2iocct  34293  icoreresf  37396  curfv  37639  ptrest  37658  poimirlem26  37685  rrnval  37866  atpsubN  39851  clsk3nimkb  44132  2arymaptf1  48753