Theorem rgen2w 3081

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

This proof depends on syntax axioms:  ∀wral 3076

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 3077

This theorem is used by:  porpss  7727  fnmpoi  8065  mptmpoopabbrd  8078  relmpoopab  8089  curfv  8871  cantnfvalf  9644  ixxf  13441  fzf  13598  fzof  13744  rexfiuz  15468  sadcf  16576  prdsvallem  17572  prdsds  17582  homfeq  17815  comfeq  17827  wunnat  18081  eldmcoa  18187  catcfuccl  18240  relxpchom  18302  catcxpccl  18328  plusffval  18769  grpsubfval  19141  lsmass  19830  efgval2  19885  dmdprd  20161  dprdval  20166  scaffval  21102  ipffval  21901  psdmul  22434  eltx  23834  xkotf  23851  txcnp  23886  txcnmpt  23890  txrest  23897  txlm  23914  txflf  24272  dscmet  24838  xrtgioo  25073  ishtpy  25240  opnmblALT  25871  zsoring  28714  tglnfn  28929  tgplnfn  29172  wwlksonvtx  30363  wspthnonp  30367  clwwlknondisj  30621  hlimreui  31760  aciunf1lem  33175  ofoprabco  33177  lsmssass  33872  dya2iocct  34832  vonf1osev  35810  mh-inf3sn  37246  icoreresf  38189  ptrest  38451  poimirlem26  38478  rrnval  38675  disjimeceqbi  39652  atpsubN  40724  clsk3nimkb  44978  2arymaptf1  49681