Theorem rgen2w 3084

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

This proof depends on syntax axioms:  ∀wral 3079

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

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

This theorem is used by:  porpss  7724  fnmpoi  8063  mptmpoopabbrd  8074  relmpoopab  8085  cantnfvalf  9630  ixxf  13386  fzf  13543  fzof  13689  rexfiuz  15404  sadcf  16515  prdsvallem  17511  prdsds  17521  homfeq  17754  comfeq  17766  wunnat  18020  eldmcoa  18126  catcfuccl  18179  relxpchom  18241  catcxpccl  18267  plusffval  18708  grpsubfval  19054  lsmass  19743  efgval2  19798  dmdprd  20074  dprdval  20079  scaffval  21010  ipffval  21807  psdmul  22338  eltx  23734  xkotf  23751  txcnp  23786  txcnmpt  23790  txrest  23797  txlm  23814  txflf  24172  dscmet  24738  xrtgioo  24973  ishtpy  25140  opnmblALT  25771  zsoring  28611  tglnfn  28825  tgplnfn  29066  wwlksonvtx  30213  wspthnonp  30217  clwwlknondisj  30471  hlimreui  31600  aciunf1lem  33016  ofoprabco  33018  lsmssass  33720  dya2iocct  34679  vonf1osev  35604  mh-inf3sn  37081  icoreresf  38026  curfv  38279  ptrest  38298  poimirlem26  38325  rrnval  38506  disjimeceqbi  39483  atpsubN  40555  clsk3nimkb  44794  2arymaptf1  49461