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

Theorem ssrab3 3909
Description: Subclass relation for a restricted class abstraction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypothesis
Ref Expression
ssrab3.1 𝐵 = {𝑥𝐴𝜑}
Assertion
Ref Expression
ssrab3 𝐵𝐴
Distinct variable group:   𝑥,𝐴
Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)

Proof of Theorem ssrab3
StepHypRef Expression
1 ssrab3.1 . 2 𝐵 = {𝑥𝐴𝜑}
2 ssrab2 3908 . 2 {𝑥𝐴𝜑} ⊆ 𝐴
31, 2eqsstri 3854 1 𝐵𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1601  {crab 3094  wss 3792
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rab 3099  df-in 3799  df-ss 3806
This theorem is referenced by:  dmmptss  5885  omsson  7347  oawordeulem  7918  ordtypelem2  8713  wemapso2lem  8746  wemapwe  8891  cplem1  9049  cofsmo  9426  fin23lem28  9497  fin23lem30  9499  isf32lem5  9514  isf32lem6  9515  isf32lem7  9516  isf32lem8  9517  hsmexlem4  9586  hsmexlem5  9587  hsmexlem6  9588  zorn2lem1  9653  zorn2lem3  9655  zorn2lem4  9656  zorn2lem5  9657  0nnq  10081  elpqn  10082  rpnnen1lem2  12124  rpssre  12144  sqrlem5  14394  dvdsflip  15446  divalglem2  15525  divalglem5  15527  divalglem8  15530  gcdcllem3  15629  bezoutlem2  15663  bezoutlem3  15664  maxprmfct  15825  phimullem  15888  eulerthlem2  15891  pclem  15947  infpn2  16021  prmreclem2  16025  prmreclem3  16026  prmreclem5  16028  4sqlem13  16065  4sqlem14  16066  4sqlem17  16069  4sqlem18  16070  vdwnnlem3  16105  ramcl2lem  16117  ramtcl  16118  ramtcl2  16119  ramtub  16120  imasdsval2  16562  gsumval1  17663  nmzsubg  18019  nmznsg  18022  usgrres  26655  frgrwopregbsn  27725  frgrwopreg1  27726  eulerpartlemgvv  31036  reprpmtf1o  31306  hgt750lemb  31336  hgt750leme  31338  bnj1212  31469  bnj213  31551  bnj1286  31686  bnj1312  31725  bnj1523  31738  limcperiod  40768  cncfshift  41015  cncfperiod  41020
  Copyright terms: Public domain W3C validator