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  6397  f2ndres  6398  exmidonfinlem  7551  netap  7626  2onetap  7627  2omotaplemap  7629  mpomulf  8322  aptap  8986  zfidc  9732  fcdmnn0fsuppfi  9743  divfnzn  10036  fnpfx  11470  wrd2ind  11516  1arith  13174  ballotfilem2  13285  xpsff1o  13728  mgmidmo  13750  nmznsg  14074  isabli  14192  rhmfn  14587  cnsubmlem  15023  cnsubrglem  15025  txuni2  15499  divcnap  15808  abscncf  15828  recncf  15829  imcncf  15830  cjcncf  15831  reefiso  16020  ioocosf1o  16099  sgmf  16272  perfectlem2  16317  2lgslem1b  16430