Theorem rgen2 2958

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

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977  ∀wral 2896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827

This theorem depends on definitions:  df-bi 196  df-an 385  df-ral 2901

This theorem is referenced by:  rgen3  2959  invdisjrab  4572  f1stres  7081  f2ndres  7082  smobeth  9287  wrd2ind  13329  smupf  15038  xpsff1o  16051  efgmf  17949  efglem  17952  txuni2  21178  divcn  22479  abscncf  22512  recncf  22513  imcncf  22514  cjcncf  22515  cnllycmp  22563  bndth  22565  dyadf  23165  cxpcn3  24289  sgmf  24671  2lgslem1b  24917  smcnlem  26936  helch  27484  hsn0elch  27489  hhshsslem2  27509  shscli  27560  shintcli  27572  0cnop  28222  0cnfn  28223  idcnop  28224  lnophsi  28244  nlelshi  28303  cnlnadjlem6  28315  cnzh  29342  rezh  29343  cnllyscon  30481  rellyscon  30487  fneref  31515  dnicn  31652  mblfinlem1  32616  mblfinlem2  32617  frmx  36496  frmy  36497  fmtnof1  39985  2wspiundisj  41166  2wspmdisj  41501  2zrngnmrid  41740  ldepslinc  42092