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

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