Theorem ssrab3 4038

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

Syntax hints:   = wceq 1563  {crab 3417   ⊆ wss 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-ss 3924

This theorem is referenced by:  dmmptss  6231  omsson  7854  oawordeulem  8527  ordtypelem2  9469  wemapso2lem  9502  wemapwe  9654  scottss  9857  cplem1  9863  cofsmo  10241  fin23lem28  10312  fin23lem30  10314  isf32lem5  10329  isf32lem6  10330  isf32lem7  10331  isf32lem8  10332  hsmexlem4  10401  hsmexlem5  10402  hsmexlem6  10403  zorn2lem1  10468  zorn2lem3  10470  zorn2lem4  10471  zorn2lem5  10472  0nnq  10897  elpqn  10898  rpnnen1lem2  12989  rpssre  13012  01sqrexlem5  15285  dvdsflip  16363  divalglem2  16441  divalglem5  16443  divalglem8  16446  gcdcllem3  16547  bezoutlem2  16586  bezoutlem3  16587  maxprmfct  16756  phimullem  16826  eulerthlem2  16829  pclem  16886  infpn2  16961  prmreclem2  16965  prmreclem3  16966  prmreclem5  16968  4sqlem13  17005  4sqlem14  17006  4sqlem17  17009  4sqlem18  17010  vdwnnlem3  17045  ramcl2lem  17057  ramtcl  17058  ramtcl2  17059  ramtub  17060  imasdsval2  17558  gsumval1  18729  nmzsubg  19219  nmznsg  19222  conjnmz  19310  conjnmzb  19311  gastacl  19367  sylow1lem2  19657  sylow1lem3  19658  sylow1lem4  19659  sylow1lem5  19660  sylow2a  19677  sylow3lem2  19686  ablfacrplem  20125  ablfacrp2  20127  ablfac1eu  20133  pgpfaclem1  20141  ablfaclem2  20146  ablfaclem3  20147  nzrring  20587  lringnzr  20614  rrgeq0  20773  rrgss  20775  lspsolvlem  21232  lbsextlem2  21249  lbsextlem3  21250  lbsextlem4  21251  ssdifidllem  21441  ssdifidlprm  21443  cygznlem2a  21674  psgnghm  21687  dsmmbase  21842  frlmsslsp  21903  psrbagconf1o  22036  psrass1lem  22040  mplbasss  22103  coe1mul2lem2  22386  mretopd  23206  hauscmplem  23520  ptcmplem1  24166  ptcmplem3  24168  tgpconncompeqg  24226  imasdsf1olem  24487  blcld  24619  icccmplem1  24937  icccmplem2  24938  icccmplem3  24939  rrxf  25517  ivthlem1  25567  ivthlem2  25568  ivthlem3  25569  ovolsslem  25600  ovolicc2lem3  25635  ovolicc2lem4  25636  ovolicc2lem5  25637  ovolicc2  25638  dyadmbllem  25715  dyadmbl  25716  iblmbf  25883  abelthlem4  26551  abelthlem6  26553  abelthlem9  26557  abelth  26558  dvatan  27054  atancn  27055  lgamucov  27156  lgamucov2  27157  ftalem3  27193  mpodvdsmulf1o  27312  fsumdvdsmul  27313  dvdsmulf1o  27314  lgsfcl2  27421  rpvmasum2  27630  dchrisum0re  27631  dchrisum0lema  27632  dchrisum0lem1b  27633  dchrisum0lem1  27634  dchrisum0lem2a  27635  dchrisum0lem2  27636  dchrisum0lem3  27637  dchrisum0  27638  pntlem3  27727  axcontlem2  29220  axcontlem7  29225  axcontlem8  29226  axcontlem10  29228  upgrreslem  29559  umgrreslem  29560  usgrres  29563  vtxdginducedm1lem2  29795  finsumvtxdg2ssteplem1  29800  clwwlksswrd  30243  frgrwopregbsn  30573  frgrwopreg1  30574  atssch  32600  partfun2  32929  fcobijfs  32974  fcobijfs2  32975  elrgspnlem1  33470  elrgspnlem2  33471  nsgmgc  33632  ssmxidllem  33668  1arithufdlem2  33747  1arithufdlem4  33749  extvfvvcl  33837  mplmulmvr  33841  psrmonprod  33854  esplymhp  33870  esplyfv1  33871  esplysply  33873  esplyfval3  33874  esplyind  33877  eulerpartlemgvv  34678  reprpmtf1o  34925  hgt750lemb  34955  hgt750leme  34957  bnj1212  35099  bnj213  35182  bnj1286  35319  bnj1312  35358  bnj1523  35371  subfacp1lem3  35540  subfacp1lem5  35542  wlimss  36185  bj-smgrpssmgm  37767  bj-mndsssmgrp  37769  bj-cmnssmnd  37771  bj-grpssmnd  37773  aks6d1c6lem4  42797  readvcot  42980  evlsmhpvvval  43184  fglmod  43657  naddwordnexlem4  43985  limcperiod  46203  cncfshift  46447  cncfperiod  46452  ovnsslelem  47133  ovolval5lem3  47227  uspgrlimlem2  48610  uspgrlim  48613