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

Theorem rabssdv 3988
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 1121 . . 3 (𝜑 → (𝑥𝐴 → (𝜓𝑥𝐵)))
32ralrimiv 3104 . 2 (𝜑 → ∀𝑥𝐴 (𝜓𝑥𝐵))
4 rabss 3985 . 2 ({𝑥𝐴𝜓} ⊆ 𝐵 ↔ ∀𝑥𝐴 (𝜓𝑥𝐵))
53, 4sylibr 237 1 (𝜑 → {𝑥𝐴𝜓} ⊆ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1089  wcel 2110  wral 3061  {crab 3065  wss 3866
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-ex 1788  df-nf 1792  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ral 3066  df-rab 3070  df-v 3410  df-in 3873  df-ss 3883
This theorem is referenced by:  suppss2  7942  oemapvali  9299  cantnflem1  9304  harval2  9613  zsupss  12533  ramub1lem1  16579  symggen  18862  efgsfo  19129  ablfacrp  19453  ablfac1eu  19460  pgpfac1lem5  19466  ablfaclem3  19474  nrmr0reg  22646  ptcmplem3  22951  abelthlem2  25324  lgamgulmlem1  25911  rspectopn  31531  neibastop2lem  34286  topmeet  34290  cntotbnd  35691  mapdrvallem2  39396  k0004ss1  41438  liminfvalxr  42999
  Copyright terms: Public domain W3C validator