Theorem rgen2w 3083

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

This proof depends on syntax axioms:  ∀wral 3078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828

This proof depends on definitions:  df-bi 210  df-ral 3079

This theorem is used by:  porpss  7731  fnmpoi  8070  mptmpoopabbrd  8083  relmpoopab  8094  curfv  8874  cantnfvalf  9647  ixxf  13408  fzf  13565  fzof  13711  rexfiuz  15435  sadcf  16545  prdsvallem  17541  prdsds  17551  homfeq  17784  comfeq  17796  wunnat  18050  eldmcoa  18156  catcfuccl  18209  relxpchom  18271  catcxpccl  18297  plusffval  18738  grpsubfval  19106  lsmass  19795  efgval2  19850  dmdprd  20126  dprdval  20131  scaffval  21063  ipffval  21860  psdmul  22393  eltx  23793  xkotf  23810  txcnp  23845  txcnmpt  23849  txrest  23856  txlm  23873  txflf  24231  dscmet  24797  xrtgioo  25032  ishtpy  25199  opnmblALT  25830  zsoring  28670  tglnfn  28885  tgplnfn  29128  wwlksonvtx  30307  wspthnonp  30311  clwwlknondisj  30565  hlimreui  31704  aciunf1lem  33120  ofoprabco  33122  lsmssass  33816  dya2iocct  34776  vonf1osev  35694  mh-inf3sn  37146  icoreresf  38091  ptrest  38353  poimirlem26  38380  rrnval  38562  disjimeceqbi  39539  atpsubN  40611  clsk3nimkb  44865  2arymaptf1  49568