Theorem ssrab3 4023

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

Syntax hints:   = wceq 1542  {crab 3390   ⊆ wss 3890

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 3391  df-ss 3907

This theorem is referenced by:  dmmptss  6199  omsson  7814  oawordeulem  8482  ordtypelem2  9427  wemapso2lem  9460  wemapwe  9609  cplem1  9804  cofsmo  10182  fin23lem28  10253  fin23lem30  10255  isf32lem5  10270  isf32lem6  10271  isf32lem7  10272  isf32lem8  10273  hsmexlem4  10342  hsmexlem5  10343  hsmexlem6  10344  zorn2lem1  10409  zorn2lem3  10411  zorn2lem4  10412  zorn2lem5  10413  0nnq  10838  elpqn  10839  rpnnen1lem2  12918  rpssre  12941  01sqrexlem5  15199  dvdsflip  16277  divalglem2  16355  divalglem5  16357  divalglem8  16360  gcdcllem3  16461  bezoutlem2  16500  bezoutlem3  16501  maxprmfct  16670  phimullem  16740  eulerthlem2  16743  pclem  16800  infpn2  16875  prmreclem2  16879  prmreclem3  16880  prmreclem5  16882  4sqlem13  16919  4sqlem14  16920  4sqlem17  16923  4sqlem18  16924  vdwnnlem3  16959  ramcl2lem  16971  ramtcl  16972  ramtcl2  16973  ramtub  16974  imasdsval2  17471  gsumval1  18642  nmzsubg  19131  nmznsg  19134  conjnmz  19218  conjnmzb  19219  gastacl  19275  sylow1lem2  19565  sylow1lem3  19566  sylow1lem4  19567  sylow1lem5  19568  sylow2a  19585  sylow3lem2  19594  ablfacrplem  20033  ablfacrp2  20035  ablfac1eu  20041  pgpfaclem1  20049  ablfaclem2  20054  ablfaclem3  20055  nzrring  20484  lringnzr  20509  rrgeq0  20668  rrgss  20670  lspsolvlem  21132  lbsextlem2  21149  lbsextlem3  21150  lbsextlem4  21151  cygznlem2a  21557  psgnghm  21570  dsmmbase  21725  frlmsslsp  21786  psrbagconf1o  21919  psrass1lem  21922  mplbasss  21985  coe1mul2lem2  22243  mretopd  23067  hauscmplem  23381  ptcmplem1  24027  ptcmplem3  24029  tgpconncompeqg  24087  imasdsf1olem  24348  blcld  24480  icccmplem1  24798  icccmplem2  24799  icccmplem3  24800  rrxf  25378  ivthlem1  25428  ivthlem2  25429  ivthlem3  25430  ovolsslem  25461  ovolicc2lem3  25496  ovolicc2lem4  25497  ovolicc2lem5  25498  ovolicc2  25499  dyadmbllem  25576  dyadmbl  25577  iblmbf  25744  abelthlem4  26412  abelthlem6  26414  abelthlem9  26418  abelth  26419  dvatan  26912  atancn  26913  lgamucov  27015  lgamucov2  27016  ftalem3  27052  mpodvdsmulf1o  27171  fsumdvdsmul  27172  dvdsmulf1o  27173  lgsfcl2  27280  rpvmasum2  27489  dchrisum0re  27490  dchrisum0lema  27491  dchrisum0lem1b  27492  dchrisum0lem1  27493  dchrisum0lem2a  27494  dchrisum0lem2  27495  dchrisum0lem3  27496  dchrisum0  27497  pntlem3  27586  axcontlem2  29048  axcontlem7  29053  axcontlem8  29054  axcontlem10  29056  upgrreslem  29387  umgrreslem  29388  usgrres  29391  vtxdginducedm1lem2  29624  finsumvtxdg2ssteplem1  29629  clwwlksswrd  30072  frgrwopregbsn  30402  frgrwopreg1  30403  atssch  32429  partfun2  32764  fcobijfs  32809  fcobijfs2  32810  elrgspnlem1  33318  elrgspnlem2  33319  nsgmgc  33487  ssdifidllem  33531  ssdifidlprm  33533  ssmxidllem  33548  1arithufdlem2  33620  1arithufdlem4  33622  extvfvvcl  33694  mplmulmvr  33698  psrmonprod  33711  esplymhp  33727  esplyfv1  33728  esplysply  33730  esplyfval3  33731  esplyind  33734  eulerpartlemgvv  34536  reprpmtf1o  34786  hgt750lemb  34816  hgt750leme  34818  bnj1212  34957  bnj213  35040  bnj1286  35177  bnj1312  35216  bnj1523  35229  subfacp1lem3  35380  subfacp1lem5  35382  wlimss  36025  bj-smgrpssmgm  37598  bj-mndsssmgrp  37600  bj-cmnssmnd  37602  bj-grpssmnd  37604  aks6d1c6lem4  42626  readvcot  42810  evlsmhpvvval  43042  fglmod  43519  naddwordnexlem4  43847  scottss  44688  limcperiod  46076  cncfshift  46320  cncfperiod  46325  ovnsslelem  47006  ovolval5lem3  47100  uspgrlimlem2  48477  uspgrlim  48480