Theorem ssrab3 4008

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 4007	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴
3	1, 2	eqsstri 3949	1 ⊢ 𝐵 ⊆ 𝐴

Syntax hints:   = wceq 1538  {crab 3110   ⊆ wss 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  dmmptss  6062  omsson  7564  oawordeulem  8163  ordtypelem2  8967  wemapso2lem  9000  wemapwe  9144  cplem1  9302  cofsmo  9680  fin23lem28  9751  fin23lem30  9753  isf32lem5  9768  isf32lem6  9769  isf32lem7  9770  isf32lem8  9771  hsmexlem4  9840  hsmexlem5  9841  hsmexlem6  9842  zorn2lem1  9907  zorn2lem3  9909  zorn2lem4  9910  zorn2lem5  9911  0nnq  10335  elpqn  10336  rpnnen1lem2  12364  rpssre  12384  sqrlem5  14598  dvdsflip  15659  divalglem2  15736  divalglem5  15738  divalglem8  15741  gcdcllem3  15840  bezoutlem2  15878  bezoutlem3  15879  maxprmfct  16043  phimullem  16106  eulerthlem2  16109  pclem  16165  infpn2  16239  prmreclem2  16243  prmreclem3  16244  prmreclem5  16246  4sqlem13  16283  4sqlem14  16284  4sqlem17  16287  4sqlem18  16288  vdwnnlem3  16323  ramcl2lem  16335  ramtcl  16336  ramtcl2  16337  ramtub  16338  imasdsval2  16781  gsumval1  17885  nmzsubg  18309  nmznsg  18312  conjnmz  18384  conjnmzb  18385  gastacl  18431  sylow1lem2  18716  sylow1lem3  18717  sylow1lem4  18718  sylow1lem5  18719  sylow2a  18736  sylow3lem2  18745  ablfacrplem  19180  ablfacrp2  19182  ablfac1eu  19188  pgpfaclem1  19196  ablfaclem2  19201  ablfaclem3  19202  lspsolvlem  19907  lbsextlem2  19924  lbsextlem3  19925  lbsextlem4  19926  rrgeq0  20056  rrgss  20058  cygznlem2a  20259  psgnghm  20269  dsmmbase  20424  frlmsslsp  20485  psrbagconf1o  20612  psrass1lem  20615  mplbasss  20670  coe1mul2lem2  20897  mretopd  21697  hauscmplem  22011  ptcmplem1  22657  ptcmplem3  22659  tgpconncompeqg  22717  imasdsf1olem  22980  blcld  23112  icccmplem1  23427  icccmplem2  23428  icccmplem3  23429  rrxf  24005  ivthlem1  24055  ivthlem2  24056  ivthlem3  24057  ovolsslem  24088  ovolicc2lem3  24123  ovolicc2lem4  24124  ovolicc2lem5  24125  ovolicc2  24126  dyadmbllem  24203  dyadmbl  24204  iblmbf  24371  abelthlem4  25029  abelthlem6  25031  abelthlem9  25035  abelth  25036  dvatan  25521  atancn  25522  lgamucov  25623  lgamucov2  25624  ftalem3  25660  dvdsmulf1o  25779  fsumdvdsmul  25780  lgsfcl2  25887  rpvmasum2  26096  dchrisum0re  26097  dchrisum0lema  26098  dchrisum0lem1b  26099  dchrisum0lem1  26100  dchrisum0lem2a  26101  dchrisum0lem2  26102  dchrisum0lem3  26103  dchrisum0  26104  pntlem3  26193  axcontlem2  26759  axcontlem7  26764  axcontlem8  26765  axcontlem10  26767  upgrreslem  27094  umgrreslem  27095  usgrres  27098  vtxdginducedm1lem2  27330  finsumvtxdg2ssteplem1  27335  clwwlksswrd  27772  frgrwopregbsn  28102  frgrwopreg1  28103  atssch  30126  ssmxidllem  31049  eulerpartlemgvv  31744  reprpmtf1o  32007  hgt750lemb  32037  hgt750leme  32039  bnj1212  32181  bnj213  32264  bnj1286  32401  bnj1312  32440  bnj1523  32453  wlimss  33229  bj-smgrpssmgm  34683  bj-mndsssmgrp  34685  bj-cmnssmnd  34687  bj-grpssmnd  34689  fglmod  40017  scottss  40951  limcperiod  42270  cncfshift  42516  cncfperiod  42521