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

Theorem rabssdv 4085
Description: Subclass of a restricted class abstraction (deduction form). (Contributed by NM, 2-Feb-2015.)
Hypothesis
Ref Expression
rabssdv.1 ((𝜑𝑥𝐴𝜓) → 𝑥𝐵)
Assertion
Ref Expression
rabssdv (𝜑 → {𝑥𝐴𝜓} ⊆ 𝐵)
Distinct variable groups:   𝑥,𝐵   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem rabssdv
StepHypRef Expression
1 rabssdv.1 . . . 4 ((𝜑𝑥𝐴𝜓) → 𝑥𝐵)
213exp 1118 . . 3 (𝜑 → (𝑥𝐴 → (𝜓𝑥𝐵)))
32ralrimiv 3143 . 2 (𝜑 → ∀𝑥𝐴 (𝜓𝑥𝐵))
4 rabss 4082 . 2 ({𝑥𝐴𝜓} ⊆ 𝐵 ↔ ∀𝑥𝐴 (𝜓𝑥𝐵))
53, 4sylibr 234 1 (𝜑 → {𝑥𝐴𝜓} ⊆ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1086  wcel 2106  wral 3059  {crab 3433  wss 3963
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-ex 1777  df-nf 1781  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ral 3060  df-rab 3434  df-ss 3980
This theorem is referenced by:  suppss2  8224  oemapvali  9722  cantnflem1  9727  harval2  10035  zsupss  12977  ramub1lem1  17060  symggen  19503  efgsfo  19772  ablfacrp  20101  ablfac1eu  20108  pgpfac1lem5  20114  ablfaclem3  20122  nrmr0reg  23773  ptcmplem3  24078  abelthlem2  26491  lgamgulmlem1  27087  sltonold  28298  rspectopn  33828  neibastop2lem  36343  topmeet  36347  weiunse  36451  cntotbnd  37783  mapdrvallem2  41628  aks6d1c6lem3  42154  onintunirab  43216  nadd2rabex  43376  k0004ss1  44141  liminfvalxr  45739
  Copyright terms: Public domain W3C validator