Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  rgen2 Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 rgen2.1 . . 3 ((𝑥𝐴𝑦𝐵) → 𝜑)
21ralrimiva 3104 . 2 (𝑥𝐴 → ∀𝑦𝐵 𝜑)
32rgen 3060 1 𝑥𝐴𝑦𝐵 𝜑
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator