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  7545  netap  7620  2onetap  7621  2omotaplemap  7623  mpomulf  8316  aptap  8980  zfidc  9727  divfnzn  10030  fnpfx  11463  wrd2ind  11509  1arith  13166  ballotfilem2  13277  xpsff1o  13719  mgmidmo  13741  nmznsg  14065  isabli  14152  rhmfn  14528  cnsubmlem  14964  cnsubrglem  14966  txuni2  15406  divcnap  15715  abscncf  15735  recncf  15736  imcncf  15737  cjcncf  15738  reefiso  15927  ioocosf1o  16005  sgmf  16167  perfectlem2  16198  2lgslem1b  16306