Theorem rgen2w 3064

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

Syntax hints:  ∀wral 3059

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

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

This theorem is referenced by:  porpss  7746  fnmpoi  8094  mptmpoopabbrd  8104  relmpoopab  8118  cantnfvalf  9703  ixxf  13394  fzf  13548  fzof  13693  rexfiuz  15383  sadcf  16487  prdsvallem  17501  prdsds  17511  homfeq  17739  comfeq  17751  wunnat  18011  wunnatOLD  18012  eldmcoa  18119  catcfuccl  18173  catcfucclOLD  18174  relxpchom  18237  catcxpccl  18263  catcxpcclOLD  18264  plusffval  18672  grpsubfval  19014  lsmass  19702  efgval2  19757  dmdprd  20033  dprdval  20038  scaffval  20895  ipffval  21684  psdmul  22188  eltx  23592  xkotf  23609  txcnp  23644  txcnmpt  23648  txrest  23655  txlm  23672  txflf  24030  dscmet  24601  xrtgioo  24842  ishtpy  25018  opnmblALT  25652  tglnfn  28570  wwlksonvtx  29885  wspthnonp  29889  clwwlknondisj  30140  hlimreui  31268  aciunf1lem  32679  ofoprabco  32681  lsmssass  33410  dya2iocct  34262  icoreresf  37335  curfv  37587  ptrest  37606  poimirlem26  37633  rrnval  37814  atpsubN  39736  clsk3nimkb  44030  2arymaptf1  48503