Theorem rgen2 2593

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2177  ∀wral 2485

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-ral 2490

This theorem is referenced by:  rgen3  2594  invdisjrab  4045  f1stres  6258  f2ndres  6259  exmidonfinlem  7317  netap  7386  2onetap  7387  2omotaplemap  7389  mpomulf  8082  aptap  8743  divfnzn  9762  fnpfx  11153  wrd2ind  11199  1arith  12765  xpsff1o  13256  mgmidmo  13279  nmznsg  13624  isabli  13711  rhmfn  14009  cnsubmlem  14415  cnsubrglem  14417  txuni2  14803  divcnap  15112  abscncf  15132  recncf  15133  imcncf  15134  cjcncf  15135  reefiso  15324  ioocosf1o  15401  sgmf  15533  perfectlem2  15547  2lgslem1b  15641