Theorem rgen2w 3066

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

Syntax hints:  ∀wral 3061

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 3062

This theorem is referenced by:  porpss  7747  fnmpoi  8095  mptmpoopabbrd  8105  relmpoopab  8119  cantnfvalf  9705  ixxf  13397  fzf  13551  fzof  13696  rexfiuz  15386  sadcf  16490  prdsvallem  17499  prdsds  17509  homfeq  17737  comfeq  17749  wunnat  18004  eldmcoa  18110  catcfuccl  18163  relxpchom  18226  catcxpccl  18252  plusffval  18659  grpsubfval  19001  lsmass  19687  efgval2  19742  dmdprd  20018  dprdval  20023  scaffval  20878  ipffval  21666  psdmul  22170  eltx  23576  xkotf  23593  txcnp  23628  txcnmpt  23632  txrest  23639  txlm  23656  txflf  24014  dscmet  24585  xrtgioo  24828  ishtpy  25004  opnmblALT  25638  tglnfn  28555  wwlksonvtx  29875  wspthnonp  29879  clwwlknondisj  30130  hlimreui  31258  aciunf1lem  32672  ofoprabco  32674  lsmssass  33430  dya2iocct  34282  icoreresf  37353  curfv  37607  ptrest  37626  poimirlem26  37653  rrnval  37834  atpsubN  39755  clsk3nimkb  44053  2arymaptf1  48574