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  7674  fnmpoi  8016  mptmpoopabbrd  8026  relmpoopab  8038  cantnfvalf  9578  ixxf  13275  fzf  13431  fzof  13576  rexfiuz  15275  sadcf  16384  prdsvallem  17378  prdsds  17388  homfeq  17621  comfeq  17633  wunnat  17887  eldmcoa  17993  catcfuccl  18046  relxpchom  18108  catcxpccl  18134  plusffval  18575  grpsubfval  18917  lsmass  19602  efgval2  19657  dmdprd  19933  dprdval  19938  scaffval  20835  ipffval  21607  psdmul  22113  eltx  23516  xkotf  23533  txcnp  23568  txcnmpt  23572  txrest  23579  txlm  23596  txflf  23954  dscmet  24520  xrtgioo  24755  ishtpy  24931  opnmblALT  25564  zsoring  28409  tglnfn  28623  wwlksonvtx  29932  wspthnonp  29936  clwwlknondisj  30190  hlimreui  31318  aciunf1lem  32743  ofoprabco  32745  lsmssass  33485  dya2iocct  34439  icoreresf  37559  curfv  37803  ptrest  37822  poimirlem26  37849  rrnval  38030  disjimeceqbi  39009  atpsubN  40081  clsk3nimkb  44348  2arymaptf1  48966