Theorem ssrab3 4032

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

Syntax hints:   = wceq 1541  {crab 3395   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-ss 3919

This theorem is referenced by:  dmmptss  6188  omsson  7800  oawordeulem  8469  ordtypelem2  9405  wemapso2lem  9438  wemapwe  9587  cplem1  9782  cofsmo  10160  fin23lem28  10231  fin23lem30  10233  isf32lem5  10248  isf32lem6  10249  isf32lem7  10250  isf32lem8  10251  hsmexlem4  10320  hsmexlem5  10321  hsmexlem6  10322  zorn2lem1  10387  zorn2lem3  10389  zorn2lem4  10390  zorn2lem5  10391  0nnq  10815  elpqn  10816  rpnnen1lem2  12875  rpssre  12898  01sqrexlem5  15153  dvdsflip  16228  divalglem2  16306  divalglem5  16308  divalglem8  16311  gcdcllem3  16412  bezoutlem2  16451  bezoutlem3  16452  maxprmfct  16620  phimullem  16690  eulerthlem2  16693  pclem  16750  infpn2  16825  prmreclem2  16829  prmreclem3  16830  prmreclem5  16832  4sqlem13  16869  4sqlem14  16870  4sqlem17  16873  4sqlem18  16874  vdwnnlem3  16909  ramcl2lem  16921  ramtcl  16922  ramtcl2  16923  ramtub  16924  imasdsval2  17420  gsumval1  18591  nmzsubg  19078  nmznsg  19081  conjnmz  19165  conjnmzb  19166  gastacl  19222  sylow1lem2  19512  sylow1lem3  19513  sylow1lem4  19514  sylow1lem5  19515  sylow2a  19532  sylow3lem2  19541  ablfacrplem  19980  ablfacrp2  19982  ablfac1eu  19988  pgpfaclem1  19996  ablfaclem2  20001  ablfaclem3  20002  nzrring  20432  lringnzr  20457  rrgeq0  20616  rrgss  20618  lspsolvlem  21080  lbsextlem2  21097  lbsextlem3  21098  lbsextlem4  21099  cygznlem2a  21505  psgnghm  21518  dsmmbase  21673  frlmsslsp  21734  psrbagconf1o  21867  psrass1lem  21870  mplbasss  21935  coe1mul2lem2  22183  mretopd  23008  hauscmplem  23322  ptcmplem1  23968  ptcmplem3  23970  tgpconncompeqg  24028  imasdsf1olem  24289  blcld  24421  icccmplem1  24739  icccmplem2  24740  icccmplem3  24741  rrxf  25329  ivthlem1  25380  ivthlem2  25381  ivthlem3  25382  ovolsslem  25413  ovolicc2lem3  25448  ovolicc2lem4  25449  ovolicc2lem5  25450  ovolicc2  25451  dyadmbllem  25528  dyadmbl  25529  iblmbf  25696  abelthlem4  26372  abelthlem6  26374  abelthlem9  26378  abelth  26379  dvatan  26873  atancn  26874  lgamucov  26976  lgamucov2  26977  ftalem3  27013  mpodvdsmulf1o  27132  fsumdvdsmul  27133  dvdsmulf1o  27134  fsumdvdsmulOLD  27135  lgsfcl2  27242  rpvmasum2  27451  dchrisum0re  27452  dchrisum0lema  27453  dchrisum0lem1b  27454  dchrisum0lem1  27455  dchrisum0lem2a  27456  dchrisum0lem2  27457  dchrisum0lem3  27458  dchrisum0  27459  pntlem3  27548  axcontlem2  28944  axcontlem7  28949  axcontlem8  28950  axcontlem10  28952  upgrreslem  29283  umgrreslem  29284  usgrres  29287  vtxdginducedm1lem2  29520  finsumvtxdg2ssteplem1  29525  clwwlksswrd  29965  frgrwopregbsn  30295  frgrwopreg1  30296  atssch  32321  fcobijfs  32702  fcobijfs2  32703  elrgspnlem1  33207  elrgspnlem2  33208  nsgmgc  33375  ssdifidllem  33419  ssdifidlprm  33421  ssmxidllem  33436  1arithufdlem2  33508  1arithufdlem4  33510  esplymhp  33587  esplyfv1  33588  esplysply  33590  eulerpartlemgvv  34387  reprpmtf1o  34637  hgt750lemb  34667  hgt750leme  34669  bnj1212  34809  bnj213  34892  bnj1286  35029  bnj1312  35068  bnj1523  35081  subfacp1lem3  35224  subfacp1lem5  35226  wlimss  35869  bj-smgrpssmgm  37308  bj-mndsssmgrp  37310  bj-cmnssmnd  37312  bj-grpssmnd  37314  aks6d1c6lem4  42212  readvcot  42403  evlsmhpvvval  42634  fglmod  43112  naddwordnexlem4  43440  scottss  44282  limcperiod  45674  cncfshift  45918  cncfperiod  45923  ovnsslelem  46604  ovolval5lem3  46698  uspgrlimlem2  48026  uspgrlim  48029