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

Theorem rabss2 3669
 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 878 . . . 4 ((𝑥𝐴𝑥𝐵) → ((𝑥𝐴𝜑) → (𝑥𝐵𝜑)))
21alimi 1736 . . 3 (∀𝑥(𝑥𝐴𝑥𝐵) → ∀𝑥((𝑥𝐴𝜑) → (𝑥𝐵𝜑)))
3 dfss2 3577 . . 3 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
4 ss2ab 3654 . . 3 ({𝑥 ∣ (𝑥𝐴𝜑)} ⊆ {𝑥 ∣ (𝑥𝐵𝜑)} ↔ ∀𝑥((𝑥𝐴𝜑) → (𝑥𝐵𝜑)))
52, 3, 43imtr4i 281 . 2 (𝐴𝐵 → {𝑥 ∣ (𝑥𝐴𝜑)} ⊆ {𝑥 ∣ (𝑥𝐵𝜑)})
6 df-rab 2921 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
7 df-rab 2921 . 2 {𝑥𝐵𝜑} = {𝑥 ∣ (𝑥𝐵𝜑)}
85, 6, 73sstr4g 3630 1 (𝐴𝐵 → {𝑥𝐴𝜑} ⊆ {𝑥𝐵𝜑})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384  ∀wal 1478   ∈ wcel 1992  {cab 2612  {crab 2916   ⊆ wss 3560 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-rab 2921  df-in 3567  df-ss 3574 This theorem is referenced by:  sess2  5048  suppfnss  7266  hashbcss  15627  dprdss  18344  minveclem4  23106  prmdvdsfi  24728  mumul  24802  sqff1o  24803  rpvmasumlem  25071  disjxwwlkn  26671  clwwlksnfi  26773  shatomistici  29060  rabfodom  29182  xpinpreima2  29727  ballotth  30372  bj-unrab  32561  icorempt2  32823  lssats  33765  lpssat  33766  lssatle  33768  lssat  33769  atlatmstc  34072  dochspss  36133  rmxyelqirr  36941  idomodle  37241  sssmf  40241
 Copyright terms: Public domain W3C validator