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  4080  f1stres  6317  f2ndres  6318  exmidonfinlem  7394  netap  7463  2onetap  7464  2omotaplemap  7466  mpomulf  8159  aptap  8820  divfnzn  9845  fnpfx  11248  wrd2ind  11294  1arith  12930  xpsff1o  13422  mgmidmo  13445  nmznsg  13790  isabli  13877  rhmfn  14176  cnsubmlem  14582  cnsubrglem  14584  txuni2  14970  divcnap  15279  abscncf  15299  recncf  15300  imcncf  15301  cjcncf  15302  reefiso  15491  ioocosf1o  15568  sgmf  15700  perfectlem2  15714  2lgslem1b  15808