Theorem ssrab3 4036

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

Syntax hints:   = wceq 1542  {crab 3401   ⊆ wss 3903

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-ss 3920

This theorem is referenced by:  dmmptss  6207  omsson  7822  oawordeulem  8491  ordtypelem2  9436  wemapso2lem  9469  wemapwe  9618  cplem1  9813  cofsmo  10191  fin23lem28  10262  fin23lem30  10264  isf32lem5  10279  isf32lem6  10280  isf32lem7  10281  isf32lem8  10282  hsmexlem4  10351  hsmexlem5  10352  hsmexlem6  10353  zorn2lem1  10418  zorn2lem3  10420  zorn2lem4  10421  zorn2lem5  10422  0nnq  10847  elpqn  10848  rpnnen1lem2  12902  rpssre  12925  01sqrexlem5  15181  dvdsflip  16256  divalglem2  16334  divalglem5  16336  divalglem8  16339  gcdcllem3  16440  bezoutlem2  16479  bezoutlem3  16480  maxprmfct  16648  phimullem  16718  eulerthlem2  16721  pclem  16778  infpn2  16853  prmreclem2  16857  prmreclem3  16858  prmreclem5  16860  4sqlem13  16897  4sqlem14  16898  4sqlem17  16901  4sqlem18  16902  vdwnnlem3  16937  ramcl2lem  16949  ramtcl  16950  ramtcl2  16951  ramtub  16952  imasdsval2  17449  gsumval1  18620  nmzsubg  19106  nmznsg  19109  conjnmz  19193  conjnmzb  19194  gastacl  19250  sylow1lem2  19540  sylow1lem3  19541  sylow1lem4  19542  sylow1lem5  19543  sylow2a  19560  sylow3lem2  19569  ablfacrplem  20008  ablfacrp2  20010  ablfac1eu  20016  pgpfaclem1  20024  ablfaclem2  20029  ablfaclem3  20030  nzrring  20461  lringnzr  20486  rrgeq0  20645  rrgss  20647  lspsolvlem  21109  lbsextlem2  21126  lbsextlem3  21127  lbsextlem4  21128  cygznlem2a  21534  psgnghm  21547  dsmmbase  21702  frlmsslsp  21763  psrbagconf1o  21897  psrass1lem  21900  mplbasss  21964  coe1mul2lem2  22222  mretopd  23048  hauscmplem  23362  ptcmplem1  24008  ptcmplem3  24010  tgpconncompeqg  24068  imasdsf1olem  24329  blcld  24461  icccmplem1  24779  icccmplem2  24780  icccmplem3  24781  rrxf  25369  ivthlem1  25420  ivthlem2  25421  ivthlem3  25422  ovolsslem  25453  ovolicc2lem3  25488  ovolicc2lem4  25489  ovolicc2lem5  25490  ovolicc2  25491  dyadmbllem  25568  dyadmbl  25569  iblmbf  25736  abelthlem4  26412  abelthlem6  26414  abelthlem9  26418  abelth  26419  dvatan  26913  atancn  26914  lgamucov  27016  lgamucov2  27017  ftalem3  27053  mpodvdsmulf1o  27172  fsumdvdsmul  27173  dvdsmulf1o  27174  fsumdvdsmulOLD  27175  lgsfcl2  27282  rpvmasum2  27491  dchrisum0re  27492  dchrisum0lema  27493  dchrisum0lem1b  27494  dchrisum0lem1  27495  dchrisum0lem2a  27496  dchrisum0lem2  27497  dchrisum0lem3  27498  dchrisum0  27499  pntlem3  27588  axcontlem2  29050  axcontlem7  29055  axcontlem8  29056  axcontlem10  29058  upgrreslem  29389  umgrreslem  29390  usgrres  29393  vtxdginducedm1lem2  29626  finsumvtxdg2ssteplem1  29631  clwwlksswrd  30074  frgrwopregbsn  30404  frgrwopreg1  30405  atssch  32430  partfun2  32765  fcobijfs  32810  fcobijfs2  32811  elrgspnlem1  33335  elrgspnlem2  33336  nsgmgc  33504  ssdifidllem  33548  ssdifidlprm  33550  ssmxidllem  33565  1arithufdlem2  33637  1arithufdlem4  33639  extvfvvcl  33711  mplmulmvr  33715  psrmonprod  33728  esplymhp  33744  esplyfv1  33745  esplysply  33747  esplyfval3  33748  esplyind  33751  eulerpartlemgvv  34553  reprpmtf1o  34803  hgt750lemb  34833  hgt750leme  34835  bnj1212  34974  bnj213  35057  bnj1286  35194  bnj1312  35233  bnj1523  35246  subfacp1lem3  35395  subfacp1lem5  35397  wlimss  36040  bj-smgrpssmgm  37520  bj-mndsssmgrp  37522  bj-cmnssmnd  37524  bj-grpssmnd  37526  aks6d1c6lem4  42540  readvcot  42731  evlsmhpvvval  42950  fglmod  43427  naddwordnexlem4  43755  scottss  44596  limcperiod  45985  cncfshift  46229  cncfperiod  46234  ovnsslelem  46915  ovolval5lem3  47009  uspgrlimlem2  48346  uspgrlim  48349