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

Theorem rgen2 2969
 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 2960 . 2 (𝑥𝐴 → ∀𝑦𝐵 𝜑)
32rgen 2917 1 𝑥𝐴𝑦𝐵 𝜑
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384   ∈ wcel 1987  ∀wral 2907 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836 This theorem depends on definitions:  df-bi 197  df-an 386  df-ral 2912 This theorem is referenced by:  rgen3  2970  invdisjrab  4602  f1stres  7135  f2ndres  7136  smobeth  9352  wrd2ind  13415  smupf  15124  xpsff1o  16149  efgmf  18047  efglem  18050  txuni2  21278  divcn  22579  abscncf  22612  recncf  22613  imcncf  22614  cjcncf  22615  cnllycmp  22663  bndth  22665  dyadf  23265  cxpcn3  24389  sgmf  24771  2lgslem1b  25017  2wspiundisj  26724  2wspmdisj  27059  smcnlem  27398  helch  27946  hsn0elch  27951  hhshsslem2  27971  shscli  28022  shintcli  28034  0cnop  28684  0cnfn  28685  idcnop  28686  lnophsi  28706  nlelshi  28765  cnlnadjlem6  28777  cnzh  29793  rezh  29794  cnllysconn  30932  rellysconn  30938  fneref  31984  dnicn  32121  mblfinlem1  33075  mblfinlem2  33076  frmx  36955  frmy  36956  fmtnof1  40743  2zrngnmrid  41235  ldepslinc  41583
 Copyright terms: Public domain W3C validator