Theorem ssrab3 4033

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

This proof depends on syntax axioms:   = wceq 1570  {crab 3414   ⊆ wss 3902

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-ss 3919

This theorem is used by:  dmmptss  6241  omsson  7870  oawordeulem  8545  ordtypelem2  9495  wemapso2lem  9528  wemapwe  9680  scottss  9878  cplem1OLD  9894  cofsmo  10275  fin23lem28  10346  fin23lem30  10348  isf32lem5  10363  isf32lem6  10364  isf32lem7  10365  isf32lem8  10366  hsmexlem4  10435  hsmexlem5  10436  hsmexlem6  10437  zorn2lem1  10502  zorn2lem3  10504  zorn2lem4  10505  zorn2lem5  10506  0nnq  10937  elpqn  10938  rpnnen1lem2  13031  rpssre  13054  01sqrexlem5  15337  dvdsflip  16413  divalglem2  16491  divalglem5  16493  divalglem8  16496  gcdcllem3  16597  bezoutlem2  16636  bezoutlem3  16637  maxprmfct  16806  phimullem  16876  eulerthlem2  16879  pclem  16936  infpn2  17011  prmreclem2  17015  prmreclem3  17016  prmreclem5  17018  4sqlem13  17055  4sqlem14  17056  4sqlem17  17059  4sqlem18  17060  vdwnnlem3  17095  ramcl2lem  17107  ramtcl  17108  ramtcl2  17109  ramtub  17110  imasdsval2  17608  gsumval1  18791  nmzsubg  19294  nmznsg  19297  conjnmz  19385  conjnmzb  19386  gastacl  19442  sylow1lem2  19732  sylow1lem3  19733  sylow1lem4  19734  sylow1lem5  19735  sylow2a  19752  sylow3lem2  19761  ablfacrplem  20200  ablfacrp2  20202  ablfac1eu  20208  pgpfaclem1  20216  ablfaclem2  20221  ablfaclem3  20222  nzrring  20682  lringnzr  20709  rrgeq0  20868  rrgss  20870  lspsolvlem  21335  lbsextlem2  21352  lbsextlem3  21353  lbsextlem4  21354  ssdifidllem  21553  ssdifidlprm  21555  cygznlem2a  21786  psgnghm  21799  dsmmbase  21954  frlmsslsp  22015  psrbagconf1o  22150  psrass1lem  22154  mplbasss  22217  coe1mul2lem2  22500  mretopd  23323  hauscmplem  23637  ptcmplem1  24284  ptcmplem3  24286  tgpconncompeqg  24344  imasdsf1olem  24605  blcld  24737  icccmplem1  25055  icccmplem2  25056  icccmplem3  25057  rrxf  25635  ivthlem1  25685  ivthlem2  25686  ivthlem3  25687  ovolsslem  25718  ovolicc2lem3  25753  ovolicc2lem4  25754  ovolicc2lem5  25755  ovolicc2  25756  dyadmbllem  25833  dyadmbl  25834  iblmbf  26001  abelthlem4  26677  abelthlem6  26679  abelthlem9  26683  abelth  26684  dvatan  27180  atancn  27181  lgamucov  27282  lgamucov2  27283  ftalem3  27319  mpodvdsmulf1o  27438  fsumdvdsmul  27439  dvdsmulf1o  27440  lgsfcl2  27547  rpvmasum2  27756  dchrisum0re  27757  dchrisum0lema  27758  dchrisum0lem1b  27759  dchrisum0lem1  27760  dchrisum0lem2a  27761  dchrisum0lem2  27762  dchrisum0lem3  27763  dchrisum0  27764  pntlem3  27853  elcgrabasi  29262  axcontlem2  29430  axcontlem7  29435  axcontlem8  29436  axcontlem10  29438  upgrreslem  29772  umgrreslem  29773  usgrres  29776  vtxdginducedm1lem2  30008  finsumvtxdg2ssteplem1  30013  clwwlksswrd  30465  frgrwopregbsn  30805  frgrwopreg1  30806  atssch  32832  partfun2  33157  fcobijfs  33200  fcobijfs2  33201  elrgspnlem1  33690  elrgspnlem2  33691  nsgmgc  33849  ssmxidllem  33884  1arithufdlem2  33963  1arithufdlem4  33965  extvfvvcl  34053  mplmulmvr  34057  psrmonprod  34070  esplymhp  34086  esplyfv1  34087  esplysply  34089  esplyfval3  34090  esplyind  34093  eulerpartlemgvv  34895  reprpmtf1o  35142  hgt750lemb  35172  hgt750leme  35174  bnj1212  35316  bnj213  35399  bnj1286  35536  bnj1312  35575  bnj1523  35588  subfacp1lem3  35769  subfacp1lem5  35771  wlimss  36414  bj-smgrpssmgm  38028  bj-mndsssmgrp  38030  bj-cmnssmnd  38032  bj-grpssmnd  38034  aks6d1c6lem4  43047  readvcot  43247  evlsmhpvvval  43449  fglmod  43922  naddwordnexlem4  44250  limcperiod  46466  cncfshift  46710  cncfperiod  46715  ovnsslelem  47396  ovolval5lem3  47490  uspgrlimlem2  48913  uspgrlim  48916