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

Theorem rabssdv 3831
 Description: Subclass of a restricted class abstraction (deduction rule). (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 1112 . . 3 (𝜑 → (𝑥𝐴 → (𝜓𝑥𝐵)))
32ralrimiv 3114 . 2 (𝜑 → ∀𝑥𝐴 (𝜓𝑥𝐵))
4 rabss 3828 . 2 ({𝑥𝐴𝜓} ⊆ 𝐵 ↔ ∀𝑥𝐴 (𝜓𝑥𝐵))
53, 4sylibr 224 1 (𝜑 → {𝑥𝐴𝜓} ⊆ 𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ w3a 1071   ∈ wcel 2145  ∀wral 3061  {crab 3065   ⊆ wss 3723 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rab 3070  df-in 3730  df-ss 3737 This theorem is referenced by:  suppss2  7481  oemapvali  8745  cantnflem1  8750  harval2  9023  zsupss  11980  ramub1lem1  15937  symggen  18097  efgsfo  18359  ablfacrp  18673  ablfac1eu  18680  pgpfac1lem5  18686  ablfaclem3  18694  nrmr0reg  21773  ptcmplem3  22078  abelthlem2  24406  lgamgulmlem1  24976  neibastop2lem  32692  topmeet  32696  cntotbnd  33927  mapdrvallem2  37455  k0004ss1  38975  liminfvalxr  40533
 Copyright terms: Public domain W3C validator