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

Theorem rabss2 4051
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 621 . . . 4 ((𝑥𝐴𝑥𝐵) → ((𝑥𝐴𝜑) → (𝑥𝐵𝜑)))
21alimi 1803 . . 3 (∀𝑥(𝑥𝐴𝑥𝐵) → ∀𝑥((𝑥𝐴𝜑) → (𝑥𝐵𝜑)))
3 dfss2 3952 . . 3 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
4 ss2ab 4036 . . 3 ({𝑥 ∣ (𝑥𝐴𝜑)} ⊆ {𝑥 ∣ (𝑥𝐵𝜑)} ↔ ∀𝑥((𝑥𝐴𝜑) → (𝑥𝐵𝜑)))
52, 3, 43imtr4i 293 . 2 (𝐴𝐵 → {𝑥 ∣ (𝑥𝐴𝜑)} ⊆ {𝑥 ∣ (𝑥𝐵𝜑)})
6 df-rab 3144 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
7 df-rab 3144 . 2 {𝑥𝐵𝜑} = {𝑥 ∣ (𝑥𝐵𝜑)}
85, 6, 73sstr4g 4009 1 (𝐴𝐵 → {𝑥𝐴𝜑} ⊆ {𝑥𝐵𝜑})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wal 1526  wcel 2105  {cab 2796  {crab 3139  wss 3933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-in 3940  df-ss 3949
This theorem is referenced by:  rabssrabd  4055  sess2  5517  hashbcss  16328  dprdss  19080  minveclem4  23962  prmdvdsfi  25611  mumul  25685  sqff1o  25686  rpvmasumlem  25990  disjxwwlkn  27619  clwwlknfi  27750  clwwlknfiOLD  27751  shatomistici  30065  rabfodom  30193  xpinpreima2  31049  ballotth  31694  bj-unrab  34141  icorempo  34514  lssats  36028  lpssat  36029  lssatle  36031  lssat  36032  atlatmstc  36335  dochspss  38394  rmxyelqirr  39385  idomodle  39674  sssmf  42892
  Copyright terms: Public domain W3C validator