Theorem rgen2 2636

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∈ wcel 2209  ∀wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is used by:  rgen3  2637  invdisjrab  4124  f1stres  6393  f2ndres  6394  exmidonfinlem  7546  netap  7621  2onetap  7622  2omotaplemap  7624  mpomulf  8317  aptap  8981  zfidc  9728  divfnzn  10031  fnpfx  11465  wrd2ind  11511  1arith  13169  ballotfilem2  13280  xpsff1o  13723  mgmidmo  13745  nmznsg  14069  isabli  14187  rhmfn  14563  cnsubmlem  14999  cnsubrglem  15001  txuni2  15448  divcnap  15757  abscncf  15777  recncf  15778  imcncf  15779  cjcncf  15780  reefiso  15969  ioocosf1o  16047  sgmf  16216  perfectlem2  16261  2lgslem1b  16374