Theorem rgen2w 3049

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

Syntax hints:  ∀wral 3044

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

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

This theorem is referenced by:  porpss  7703  fnmpoi  8049  mptmpoopabbrd  8059  relmpoopab  8073  cantnfvalf  9618  ixxf  13316  fzf  13472  fzof  13617  rexfiuz  15314  sadcf  16423  prdsvallem  17417  prdsds  17427  homfeq  17655  comfeq  17667  wunnat  17921  eldmcoa  18027  catcfuccl  18080  relxpchom  18142  catcxpccl  18168  plusffval  18573  grpsubfval  18915  lsmass  19599  efgval2  19654  dmdprd  19930  dprdval  19935  scaffval  20786  ipffval  21557  psdmul  22053  eltx  23455  xkotf  23472  txcnp  23507  txcnmpt  23511  txrest  23518  txlm  23535  txflf  23893  dscmet  24460  xrtgioo  24695  ishtpy  24871  opnmblALT  25504  tglnfn  28474  wwlksonvtx  29785  wspthnonp  29789  clwwlknondisj  30040  hlimreui  31168  aciunf1lem  32586  ofoprabco  32588  lsmssass  33373  dya2iocct  34271  icoreresf  37340  curfv  37594  ptrest  37613  poimirlem26  37640  rrnval  37821  atpsubN  39747  clsk3nimkb  44029  2arymaptf1  48642