Theorem rgen2w 3057

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

Syntax hints:  ∀wral 3052

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

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

This theorem is referenced by:  porpss  7676  fnmpoi  8018  mptmpoopabbrd  8028  relmpoopab  8039  cantnfvalf  9581  ixxf  13303  fzf  13460  fzof  13605  rexfiuz  15305  sadcf  16417  prdsvallem  17412  prdsds  17422  homfeq  17655  comfeq  17667  wunnat  17921  eldmcoa  18027  catcfuccl  18080  relxpchom  18142  catcxpccl  18168  plusffval  18609  grpsubfval  18954  lsmass  19639  efgval2  19694  dmdprd  19970  dprdval  19975  scaffval  20870  ipffval  21642  psdmul  22146  eltx  23547  xkotf  23564  txcnp  23599  txcnmpt  23603  txrest  23610  txlm  23627  txflf  23985  dscmet  24551  xrtgioo  24786  ishtpy  24953  opnmblALT  25584  zsoring  28419  tglnfn  28633  wwlksonvtx  29942  wspthnonp  29946  clwwlknondisj  30200  hlimreui  31329  aciunf1lem  32754  ofoprabco  32756  lsmssass  33481  dya2iocct  34444  mh-inf3sn  36744  icoreresf  37686  curfv  37939  ptrest  37958  poimirlem26  37985  rrnval  38166  disjimeceqbi  39145  atpsubN  40217  clsk3nimkb  44489  2arymaptf1  49145