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

Theorem rabssdv 4068
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 1116 . . 3 (𝜑 → (𝑥𝐴 → (𝜓𝑥𝐵)))
32ralrimiv 3134 . 2 (𝜑 → ∀𝑥𝐴 (𝜓𝑥𝐵))
4 rabss 4065 . 2 ({𝑥𝐴𝜓} ⊆ 𝐵 ↔ ∀𝑥𝐴 (𝜓𝑥𝐵))
53, 4sylibr 233 1 (𝜑 → {𝑥𝐴𝜓} ⊆ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1084  wcel 2098  wral 3050  {crab 3418  wss 3944
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ral 3051  df-rab 3419  df-ss 3961
This theorem is referenced by:  suppss2  8206  oemapvali  9714  cantnflem1  9719  harval2  10027  zsupss  12959  ramub1lem1  17014  symggen  19454  efgsfo  19723  ablfacrp  20052  ablfac1eu  20059  pgpfac1lem5  20065  ablfaclem3  20073  nrmr0reg  23714  ptcmplem3  24019  abelthlem2  26431  lgamgulmlem1  27026  sltonold  28223  rspectopn  33619  neibastop2lem  35995  topmeet  35999  cntotbnd  37420  mapdrvallem2  41268  aks6d1c6lem3  41794  onintunirab  42802  nadd2rabex  42962  k0004ss1  43728  liminfvalxr  45314
  Copyright terms: Public domain W3C validator