Theorem rgen2 2630

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 2617	. 2 ⊢ (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐵 𝜑)
3	2	rgen 2597	1 ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2205  ∀wral 2522

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2527

This theorem is referenced by:  rgen3  2631  invdisjrab  4108  f1stres  6366  f2ndres  6367  exmidonfinlem  7509  netap  7584  2onetap  7585  2omotaplemap  7587  mpomulf  8280  aptap  8941  zfidc  9673  divfnzn  9971  fnpfx  11394  wrd2ind  11440  1arith  13090  ballotfilem2  13172  xpsff1o  13613  mgmidmo  13635  nmznsg  13966  isabli  14053  rhmfn  14417  cnsubmlem  14852  cnsubrglem  14854  txuni2  15247  divcnap  15556  abscncf  15576  recncf  15577  imcncf  15578  cjcncf  15579  reefiso  15768  ioocosf1o  15845  sgmf  15980  perfectlem2  15994  2lgslem1b  16088