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

Step	Hyp	Ref	Expression
1		ssrab3.1	. 2 ⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜑}
2		ssrab2 3908	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴
3	1, 2	eqsstri 3854	1 ⊢ 𝐵 ⊆ 𝐴

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