Theorem rgen2 3113

Description: Generalization rule for restricted quantification, with two quantifiers. (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 3104	. 2 ⊢ (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐵 𝜑)
3	2	rgen 3060	1 ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 2139  ∀wral 3050

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988

This theorem depends on definitions:  df-bi 197  df-an 385  df-ral 3055

This theorem is referenced by:  rgen3  3114  invdisjrab  4791  f1stres  7358  f2ndres  7359  smobeth  9620  wrd2ind  13697  smupf  15422  xpsff1o  16450  efgmf  18346  efglem  18349  txuni2  21590  divcn  22892  abscncf  22925  recncf  22926  imcncf  22927  cjcncf  22928  cnllycmp  22976  bndth  22978  dyadf  23579  cxpcn3  24709  sgmf  25091  2lgslem1b  25337  smcnlem  27882  helch  28430  hsn0elch  28435  hhshsslem2  28455  shscli  28506  shintcli  28518  0cnop  29168  0cnfn  29169  idcnop  29170  lnophsi  29190  nlelshi  29249  cnlnadjlem6  29261  cnzh  30344  rezh  30345  cnllysconn  31555  rellysconn  31561  fneref  32672  dnicn  32809  mblfinlem1  33777  mblfinlem2  33778  frmx  37998  frmy  37999  fmtnof1  41975  2zrngnmrid  42478  ldepslinc  42826