Theorem rgen2 3156

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

Syntax hints:   → wi 4   ∧ wa 385   ∈ wcel 2157  ∀wral 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006

This theorem depends on definitions:  df-bi 199  df-an 386  df-ral 3094

This theorem is referenced by:  rgen3  3157  invdisjrab  4830  f1stres  7425  f2ndres  7426  smobeth  9696  wrd2ind  13778  wrd2indOLD  13779  smupf  15535  xpsff1o  16543  efgmf  18439  efglem  18442  txuni2  21697  divcn  22999  abscncf  23032  recncf  23033  imcncf  23034  cjcncf  23035  cnllycmp  23083  bndth  23085  dyadf  23699  cxpcn3  24833  sgmf  25223  2lgslem1b  25469  tgjustf  25724  smcnlem  28077  helch  28625  hsn0elch  28630  hhshsslem2  28650  shscli  28701  shintcli  28713  0cnop  29363  0cnfn  29364  idcnop  29365  lnophsi  29385  nlelshi  29444  cnlnadjlem6  29456  cnzh  30530  rezh  30531  cnllysconn  31744  rellysconn  31750  fneref  32857  dnicn  32990  mblfinlem1  33935  mblfinlem2  33936  frmx  38263  frmy  38264  fmtnof1  42229  2zrngnmrid  42749  ldepslinc  43097