Theorem ssrab3 4035

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

Syntax hints:   = wceq 1540  {crab 3396   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-ss 3922

This theorem is referenced by:  dmmptss  6194  omsson  7810  oawordeulem  8479  ordtypelem2  9430  wemapso2lem  9463  wemapwe  9612  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  10837  elpqn  10838  rpnnen1lem2  12896  rpssre  12919  01sqrexlem5  15171  dvdsflip  16246  divalglem2  16324  divalglem5  16326  divalglem8  16329  gcdcllem3  16430  bezoutlem2  16469  bezoutlem3  16470  maxprmfct  16638  phimullem  16708  eulerthlem2  16711  pclem  16768  infpn2  16843  prmreclem2  16847  prmreclem3  16848  prmreclem5  16850  4sqlem13  16887  4sqlem14  16888  4sqlem17  16891  4sqlem18  16892  vdwnnlem3  16927  ramcl2lem  16939  ramtcl  16940  ramtcl2  16941  ramtub  16942  imasdsval2  17438  gsumval1  18575  nmzsubg  19062  nmznsg  19065  conjnmz  19149  conjnmzb  19150  gastacl  19206  sylow1lem2  19496  sylow1lem3  19497  sylow1lem4  19498  sylow1lem5  19499  sylow2a  19516  sylow3lem2  19525  ablfacrplem  19964  ablfacrp2  19966  ablfac1eu  19972  pgpfaclem1  19980  ablfaclem2  19985  ablfaclem3  19986  nzrring  20419  lringnzr  20444  rrgeq0  20603  rrgss  20605  lspsolvlem  21067  lbsextlem2  21084  lbsextlem3  21085  lbsextlem4  21086  cygznlem2a  21492  psgnghm  21505  dsmmbase  21660  frlmsslsp  21721  psrbagconf1o  21854  psrass1lem  21857  mplbasss  21922  coe1mul2lem2  22170  mretopd  22995  hauscmplem  23309  ptcmplem1  23955  ptcmplem3  23957  tgpconncompeqg  24015  imasdsf1olem  24277  blcld  24409  icccmplem1  24727  icccmplem2  24728  icccmplem3  24729  rrxf  25317  ivthlem1  25368  ivthlem2  25369  ivthlem3  25370  ovolsslem  25401  ovolicc2lem3  25436  ovolicc2lem4  25437  ovolicc2lem5  25438  ovolicc2  25439  dyadmbllem  25516  dyadmbl  25517  iblmbf  25684  abelthlem4  26360  abelthlem6  26362  abelthlem9  26366  abelth  26367  dvatan  26861  atancn  26862  lgamucov  26964  lgamucov2  26965  ftalem3  27001  mpodvdsmulf1o  27120  fsumdvdsmul  27121  dvdsmulf1o  27122  fsumdvdsmulOLD  27123  lgsfcl2  27230  rpvmasum2  27439  dchrisum0re  27440  dchrisum0lema  27441  dchrisum0lem1b  27442  dchrisum0lem1  27443  dchrisum0lem2a  27444  dchrisum0lem2  27445  dchrisum0lem3  27446  dchrisum0  27447  pntlem3  27536  axcontlem2  28928  axcontlem7  28933  axcontlem8  28934  axcontlem10  28936  upgrreslem  29267  umgrreslem  29268  usgrres  29271  vtxdginducedm1lem2  29504  finsumvtxdg2ssteplem1  29509  clwwlksswrd  29949  frgrwopregbsn  30279  frgrwopreg1  30280  atssch  32305  fcobijfs  32679  elrgspnlem1  33195  elrgspnlem2  33196  nsgmgc  33362  ssdifidllem  33406  ssdifidlprm  33408  ssmxidllem  33423  1arithufdlem2  33495  1arithufdlem4  33497  eulerpartlemgvv  34346  reprpmtf1o  34596  hgt750lemb  34626  hgt750leme  34628  bnj1212  34768  bnj213  34851  bnj1286  34988  bnj1312  35027  bnj1523  35040  subfacp1lem3  35157  subfacp1lem5  35159  wlimss  35805  bj-smgrpssmgm  37244  bj-mndsssmgrp  37246  bj-cmnssmnd  37248  bj-grpssmnd  37250  aks6d1c6lem4  42149  readvcot  42340  evlsmhpvvval  42571  fglmod  43049  naddwordnexlem4  43377  scottss  44219  limcperiod  45613  cncfshift  45859  cncfperiod  45864  ovnsslelem  46545  ovolval5lem3  46639  uspgrlimlem2  47977  uspgrlim  47980