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

Theorem rabssdv 4075
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 1120 . . 3 (𝜑 → (𝑥𝐴 → (𝜓𝑥𝐵)))
32ralrimiv 3145 . 2 (𝜑 → ∀𝑥𝐴 (𝜓𝑥𝐵))
4 rabss 4072 . 2 ({𝑥𝐴𝜓} ⊆ 𝐵 ↔ ∀𝑥𝐴 (𝜓𝑥𝐵))
53, 4sylibr 234 1 (𝜑 → {𝑥𝐴𝜓} ⊆ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1087  wcel 2108  wral 3061  {crab 3436  wss 3951
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rab 3437  df-ss 3968
This theorem is referenced by:  suppss2  8225  oemapvali  9724  cantnflem1  9729  harval2  10037  zsupss  12979  ramub1lem1  17064  symggen  19488  efgsfo  19757  ablfacrp  20086  ablfac1eu  20093  pgpfac1lem5  20099  ablfaclem3  20107  nrmr0reg  23757  ptcmplem3  24062  abelthlem2  26476  lgamgulmlem1  27072  sltonold  28283  rspectopn  33866  neibastop2lem  36361  topmeet  36365  weiunse  36469  cntotbnd  37803  mapdrvallem2  41647  aks6d1c6lem3  42173  onintunirab  43239  nadd2rabex  43399  k0004ss1  44164  liminfvalxr  45798
  Copyright terms: Public domain W3C validator