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  8978  zfidc  9723  divfnzn  10021  fnpfx  11449  wrd2ind  11495  1arith  13146  ballotfilem2  13228  xpsff1o  13670  mgmidmo  13692  nmznsg  14016  isabli  14103  rhmfn  14479  cnsubmlem  14915  cnsubrglem  14917  txuni2  15357  divcnap  15666  abscncf  15686  recncf  15687  imcncf  15688  cjcncf  15689  reefiso  15878  ioocosf1o  15955  sgmf  16100  perfectlem2  16114  2lgslem1b  16208