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  4077  f1stres  6311  f2ndres  6312  exmidonfinlem  7382  netap  7451  2onetap  7452  2omotaplemap  7454  mpomulf  8147  aptap  8808  divfnzn  9828  fnpfx  11224  wrd2ind  11270  1arith  12905  xpsff1o  13397  mgmidmo  13420  nmznsg  13765  isabli  13852  rhmfn  14151  cnsubmlem  14557  cnsubrglem  14559  txuni2  14945  divcnap  15254  abscncf  15274  recncf  15275  imcncf  15276  cjcncf  15277  reefiso  15466  ioocosf1o  15543  sgmf  15675  perfectlem2  15689  2lgslem1b  15783