Theorem ssrab3 4022

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

Syntax hints:   = wceq 1542  {crab 3389   ⊆ wss 3889

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-ss 3906

This theorem is referenced by:  dmmptss  6205  omsson  7821  oawordeulem  8489  ordtypelem2  9434  wemapso2lem  9467  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  12927  rpssre  12950  01sqrexlem5  15208  dvdsflip  16286  divalglem2  16364  divalglem5  16366  divalglem8  16369  gcdcllem3  16470  bezoutlem2  16509  bezoutlem3  16510  maxprmfct  16679  phimullem  16749  eulerthlem2  16752  pclem  16809  infpn2  16884  prmreclem2  16888  prmreclem3  16889  prmreclem5  16891  4sqlem13  16928  4sqlem14  16929  4sqlem17  16932  4sqlem18  16933  vdwnnlem3  16968  ramcl2lem  16980  ramtcl  16981  ramtcl2  16982  ramtub  16983  imasdsval2  17480  gsumval1  18651  nmzsubg  19140  nmznsg  19143  conjnmz  19227  conjnmzb  19228  gastacl  19284  sylow1lem2  19574  sylow1lem3  19575  sylow1lem4  19576  sylow1lem5  19577  sylow2a  19594  sylow3lem2  19603  ablfacrplem  20042  ablfacrp2  20044  ablfac1eu  20050  pgpfaclem1  20058  ablfaclem2  20063  ablfaclem3  20064  nzrring  20493  lringnzr  20518  rrgeq0  20677  rrgss  20679  lspsolvlem  21140  lbsextlem2  21157  lbsextlem3  21158  lbsextlem4  21159  cygznlem2a  21547  psgnghm  21560  dsmmbase  21715  frlmsslsp  21776  psrbagconf1o  21909  psrass1lem  21912  mplbasss  21975  coe1mul2lem2  22233  mretopd  23057  hauscmplem  23371  ptcmplem1  24017  ptcmplem3  24019  tgpconncompeqg  24077  imasdsf1olem  24338  blcld  24470  icccmplem1  24788  icccmplem2  24789  icccmplem3  24790  rrxf  25368  ivthlem1  25418  ivthlem2  25419  ivthlem3  25420  ovolsslem  25451  ovolicc2lem3  25486  ovolicc2lem4  25487  ovolicc2lem5  25488  ovolicc2  25489  dyadmbllem  25566  dyadmbl  25567  iblmbf  25734  abelthlem4  26399  abelthlem6  26401  abelthlem9  26405  abelth  26406  dvatan  26899  atancn  26900  lgamucov  27001  lgamucov2  27002  ftalem3  27038  mpodvdsmulf1o  27157  fsumdvdsmul  27158  dvdsmulf1o  27159  lgsfcl2  27266  rpvmasum2  27475  dchrisum0re  27476  dchrisum0lema  27477  dchrisum0lem1b  27478  dchrisum0lem1  27479  dchrisum0lem2a  27480  dchrisum0lem2  27481  dchrisum0lem3  27482  dchrisum0  27483  pntlem3  27572  axcontlem2  29034  axcontlem7  29039  axcontlem8  29040  axcontlem10  29042  upgrreslem  29373  umgrreslem  29374  usgrres  29377  vtxdginducedm1lem2  29609  finsumvtxdg2ssteplem1  29614  clwwlksswrd  30057  frgrwopregbsn  30387  frgrwopreg1  30388  atssch  32414  partfun2  32749  fcobijfs  32794  fcobijfs2  32795  elrgspnlem1  33303  elrgspnlem2  33304  nsgmgc  33472  ssdifidllem  33516  ssdifidlprm  33518  ssmxidllem  33533  1arithufdlem2  33605  1arithufdlem4  33607  extvfvvcl  33679  mplmulmvr  33683  psrmonprod  33696  esplymhp  33712  esplyfv1  33713  esplysply  33715  esplyfval3  33716  esplyind  33719  eulerpartlemgvv  34520  reprpmtf1o  34770  hgt750lemb  34800  hgt750leme  34802  bnj1212  34941  bnj213  35024  bnj1286  35161  bnj1312  35200  bnj1523  35213  subfacp1lem3  35364  subfacp1lem5  35366  wlimss  36009  bj-smgrpssmgm  37582  bj-mndsssmgrp  37584  bj-cmnssmnd  37586  bj-grpssmnd  37588  aks6d1c6lem4  42612  readvcot  42796  evlsmhpvvval  43028  fglmod  43501  naddwordnexlem4  43829  scottss  44670  limcperiod  46058  cncfshift  46302  cncfperiod  46307  ovnsslelem  46988  ovolval5lem3  47082  uspgrlimlem2  48465  uspgrlim  48468