Theorem rgen2 2975

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

Syntax hints:   → wi 4   ∧ wa 384   ∈ wcel 1990  ∀wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-an 386  df-ral 2917

This theorem is referenced by:  rgen3  2976  invdisjrab  4639  f1stres  7190  f2ndres  7191  smobeth  9408  wrd2ind  13477  smupf  15200  xpsff1o  16228  efgmf  18126  efglem  18129  txuni2  21368  divcn  22671  abscncf  22704  recncf  22705  imcncf  22706  cjcncf  22707  cnllycmp  22755  bndth  22757  dyadf  23359  cxpcn3  24489  sgmf  24871  2lgslem1b  25117  smcnlem  27552  helch  28100  hsn0elch  28105  hhshsslem2  28125  shscli  28176  shintcli  28188  0cnop  28838  0cnfn  28839  idcnop  28840  lnophsi  28860  nlelshi  28919  cnlnadjlem6  28931  cnzh  30014  rezh  30015  cnllysconn  31227  rellysconn  31233  fneref  32345  dnicn  32482  mblfinlem1  33446  mblfinlem2  33447  frmx  37478  frmy  37479  fmtnof1  41447  2zrngnmrid  41950  ldepslinc  42298