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

Theorem rabssdv 4002
 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 3148 . 2 (𝜑 → ∀𝑥𝐴 (𝜓𝑥𝐵))
4 rabss 3999 . 2 ({𝑥𝐴𝜓} ⊆ 𝐵 ↔ ∀𝑥𝐴 (𝜓𝑥𝐵))
53, 4sylibr 237 1 (𝜑 → {𝑥𝐴𝜓} ⊆ 𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ w3a 1084   ∈ wcel 2111  ∀wral 3106  {crab 3110   ⊆ wss 3881 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rab 3115  df-v 3443  df-in 3888  df-ss 3898 This theorem is referenced by:  suppss2  7854  oemapvali  9138  cantnflem1  9143  harval2  9417  zsupss  12332  ramub1lem1  16359  symggen  18598  efgsfo  18865  ablfacrp  19189  ablfac1eu  19196  pgpfac1lem5  19202  ablfaclem3  19210  nrmr0reg  22368  ptcmplem3  22673  abelthlem2  25041  lgamgulmlem1  25628  rspectopn  31256  neibastop2lem  33857  topmeet  33861  cntotbnd  35274  mapdrvallem2  38981  k0004ss1  40918  liminfvalxr  42486
 Copyright terms: Public domain W3C validator