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

Theorem rabss2 3826
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 915 . . . 4 ((𝑥𝐴𝑥𝐵) → ((𝑥𝐴𝜑) → (𝑥𝐵𝜑)))
21alimi 1888 . . 3 (∀𝑥(𝑥𝐴𝑥𝐵) → ∀𝑥((𝑥𝐴𝜑) → (𝑥𝐵𝜑)))
3 dfss2 3732 . . 3 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
4 ss2ab 3811 . . 3 ({𝑥 ∣ (𝑥𝐴𝜑)} ⊆ {𝑥 ∣ (𝑥𝐵𝜑)} ↔ ∀𝑥((𝑥𝐴𝜑) → (𝑥𝐵𝜑)))
52, 3, 43imtr4i 281 . 2 (𝐴𝐵 → {𝑥 ∣ (𝑥𝐴𝜑)} ⊆ {𝑥 ∣ (𝑥𝐵𝜑)})
6 df-rab 3059 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
7 df-rab 3059 . 2 {𝑥𝐵𝜑} = {𝑥 ∣ (𝑥𝐵𝜑)}
85, 6, 73sstr4g 3787 1 (𝐴𝐵 → {𝑥𝐴𝜑} ⊆ {𝑥𝐵𝜑})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wal 1630  wcel 2139  {cab 2746  {crab 3054  wss 3715
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059  df-in 3722  df-ss 3729
This theorem is referenced by:  rabssrabd  3830  sess2  5235  suppfnssOLD  7490  hashbcss  15930  dprdss  18648  minveclem4  23423  prmdvdsfi  25053  mumul  25127  sqff1o  25128  rpvmasumlem  25396  disjxwwlkn  27052  clwwlknfi  27195  shatomistici  29550  rabfodom  29672  xpinpreima2  30283  ballotth  30929  bj-unrab  33247  icorempt2  33528  lssats  34820  lpssat  34821  lssatle  34823  lssat  34824  atlatmstc  35127  dochspss  37187  rmxyelqirr  37995  idomodle  38294  sssmf  41471
  Copyright terms: Public domain W3C validator