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 ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2209  ∀wral 2528

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579

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

This theorem is referenced by:  rgen3  2637  invdisjrab  4119  f1stres  6383  f2ndres  6384  exmidonfinlem  7535  netap  7610  2onetap  7611  2omotaplemap  7613  mpomulf  8306  aptap  8968  zfidc  9702  divfnzn  10000  fnpfx  11427  wrd2ind  11473  1arith  13124  ballotfilem2  13206  xpsff1o  13647  mgmidmo  13669  nmznsg  13993  isabli  14080  rhmfn  14452  cnsubmlem  14887  cnsubrglem  14889  txuni2  15280  divcnap  15589  abscncf  15609  recncf  15610  imcncf  15611  cjcncf  15612  reefiso  15801  ioocosf1o  15878  sgmf  16014  perfectlem2  16028  2lgslem1b  16122