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

Theorem rabssdv 4037
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 3143 . 2 (𝜑 → ∀𝑥𝐴 (𝜓𝑥𝐵))
4 rabss 4034 . 2 ({𝑥𝐴𝜓} ⊆ 𝐵 ↔ ∀𝑥𝐴 (𝜓𝑥𝐵))
53, 4sylibr 233 1 (𝜑 → {𝑥𝐴𝜓} ⊆ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1088  wcel 2107  wral 3065  {crab 3410  wss 3915
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ral 3066  df-rab 3411  df-v 3450  df-in 3922  df-ss 3932
This theorem is referenced by:  suppss2  8136  oemapvali  9627  cantnflem1  9632  harval2  9940  zsupss  12869  ramub1lem1  16905  symggen  19259  efgsfo  19528  ablfacrp  19852  ablfac1eu  19859  pgpfac1lem5  19865  ablfaclem3  19873  nrmr0reg  23116  ptcmplem3  23421  abelthlem2  25807  lgamgulmlem1  26394  rspectopn  32488  neibastop2lem  34861  topmeet  34865  cntotbnd  36284  mapdrvallem2  40137  onintunirab  41590  nadd2rabex  41731  k0004ss1  42497  liminfvalxr  44098
  Copyright terms: Public domain W3C validator