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

Theorem rabss2 4007
 Description: Subclass law for restricted abstraction. (Contributed by NM, 18-Dec-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
Assertion
Ref Expression
rabss2 (𝐴𝐵 → {𝑥𝐴𝜑} ⊆ {𝑥𝐵𝜑})
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rabss2
StepHypRef Expression
1 pm3.45 624 . . . 4 ((𝑥𝐴𝑥𝐵) → ((𝑥𝐴𝜑) → (𝑥𝐵𝜑)))
21alimi 1813 . . 3 (∀𝑥(𝑥𝐴𝑥𝐵) → ∀𝑥((𝑥𝐴𝜑) → (𝑥𝐵𝜑)))
3 dfss2 3903 . . 3 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
4 ss2ab 3989 . . 3 ({𝑥 ∣ (𝑥𝐴𝜑)} ⊆ {𝑥 ∣ (𝑥𝐵𝜑)} ↔ ∀𝑥((𝑥𝐴𝜑) → (𝑥𝐵𝜑)))
52, 3, 43imtr4i 295 . 2 (𝐴𝐵 → {𝑥 ∣ (𝑥𝐴𝜑)} ⊆ {𝑥 ∣ (𝑥𝐵𝜑)})
6 df-rab 3115 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
7 df-rab 3115 . 2 {𝑥𝐵𝜑} = {𝑥 ∣ (𝑥𝐵𝜑)}
85, 6, 73sstr4g 3962 1 (𝐴𝐵 → {𝑥𝐴𝜑} ⊆ {𝑥𝐵𝜑})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399  ∀wal 1536   ∈ wcel 2111  {cab 2776  {crab 3110   ⊆ wss 3883 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-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3444  df-in 3890  df-ss 3900 This theorem is referenced by:  rabssrabd  4012  sess2  5492  hashbcss  16350  dprdss  19165  minveclem4  24077  prmdvdsfi  25736  mumul  25810  sqff1o  25811  rpvmasumlem  26115  disjxwwlkn  27743  clwwlknfi  27874  shatomistici  30188  rabfodom  30318  xpinpreima2  31326  ballotth  31971  bj-unrab  34519  icorempo  34919  lssats  36459  lpssat  36460  lssatle  36462  lssat  36463  atlatmstc  36766  dochspss  38825  rmxyelqirr  40022  idomodle  40311  sssmf  43540
 Copyright terms: Public domain W3C validator