Theorem rgen2 2616

Description: Generalization rule for restricted quantification. (Contributed by NM, 30-May-1999.)

Hypothesis

Ref	Expression
rgen2.1	⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑)

Assertion

Ref	Expression
rgen2	⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑

Distinct variable groups:   𝑥,𝑦   𝑦,𝐴

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑥,𝑦)

Proof of Theorem rgen2

Step	Hyp	Ref	Expression
1		rgen2.1	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑)
2	1	ralrimiva 2603	. 2 ⊢ (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐵 𝜑)
3	2	rgen 2583	1 ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200  ∀wral 2508

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-gen 1495  ax-4 1556  ax-17 1572

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513

This theorem is referenced by:  rgen3  2617  invdisjrab  4076  f1stres  6303  f2ndres  6304  exmidonfinlem  7367  netap  7436  2onetap  7437  2omotaplemap  7439  mpomulf  8132  aptap  8793  divfnzn  9812  fnpfx  11204  wrd2ind  11250  1arith  12885  xpsff1o  13377  mgmidmo  13400  nmznsg  13745  isabli  13832  rhmfn  14130  cnsubmlem  14536  cnsubrglem  14538  txuni2  14924  divcnap  15233  abscncf  15253  recncf  15254  imcncf  15255  cjcncf  15256  reefiso  15445  ioocosf1o  15522  sgmf  15654  perfectlem2  15668  2lgslem1b  15762