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

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