Theorem ssrab3 4034

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

Syntax hints:   = wceq 1541  {crab 3399   ⊆ wss 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-ss 3918

This theorem is referenced by:  dmmptss  6199  omsson  7812  oawordeulem  8481  ordtypelem2  9424  wemapso2lem  9457  wemapwe  9606  cplem1  9801  cofsmo  10179  fin23lem28  10250  fin23lem30  10252  isf32lem5  10267  isf32lem6  10268  isf32lem7  10269  isf32lem8  10270  hsmexlem4  10339  hsmexlem5  10340  hsmexlem6  10341  zorn2lem1  10406  zorn2lem3  10408  zorn2lem4  10409  zorn2lem5  10410  0nnq  10835  elpqn  10836  rpnnen1lem2  12890  rpssre  12913  01sqrexlem5  15169  dvdsflip  16244  divalglem2  16322  divalglem5  16324  divalglem8  16327  gcdcllem3  16428  bezoutlem2  16467  bezoutlem3  16468  maxprmfct  16636  phimullem  16706  eulerthlem2  16709  pclem  16766  infpn2  16841  prmreclem2  16845  prmreclem3  16846  prmreclem5  16848  4sqlem13  16885  4sqlem14  16886  4sqlem17  16889  4sqlem18  16890  vdwnnlem3  16925  ramcl2lem  16937  ramtcl  16938  ramtcl2  16939  ramtub  16940  imasdsval2  17437  gsumval1  18608  nmzsubg  19094  nmznsg  19097  conjnmz  19181  conjnmzb  19182  gastacl  19238  sylow1lem2  19528  sylow1lem3  19529  sylow1lem4  19530  sylow1lem5  19531  sylow2a  19548  sylow3lem2  19557  ablfacrplem  19996  ablfacrp2  19998  ablfac1eu  20004  pgpfaclem1  20012  ablfaclem2  20017  ablfaclem3  20018  nzrring  20449  lringnzr  20474  rrgeq0  20633  rrgss  20635  lspsolvlem  21097  lbsextlem2  21114  lbsextlem3  21115  lbsextlem4  21116  cygznlem2a  21522  psgnghm  21535  dsmmbase  21690  frlmsslsp  21751  psrbagconf1o  21885  psrass1lem  21888  mplbasss  21952  coe1mul2lem2  22210  mretopd  23036  hauscmplem  23350  ptcmplem1  23996  ptcmplem3  23998  tgpconncompeqg  24056  imasdsf1olem  24317  blcld  24449  icccmplem1  24767  icccmplem2  24768  icccmplem3  24769  rrxf  25357  ivthlem1  25408  ivthlem2  25409  ivthlem3  25410  ovolsslem  25441  ovolicc2lem3  25476  ovolicc2lem4  25477  ovolicc2lem5  25478  ovolicc2  25479  dyadmbllem  25556  dyadmbl  25557  iblmbf  25724  abelthlem4  26400  abelthlem6  26402  abelthlem9  26406  abelth  26407  dvatan  26901  atancn  26902  lgamucov  27004  lgamucov2  27005  ftalem3  27041  mpodvdsmulf1o  27160  fsumdvdsmul  27161  dvdsmulf1o  27162  fsumdvdsmulOLD  27163  lgsfcl2  27270  rpvmasum2  27479  dchrisum0re  27480  dchrisum0lema  27481  dchrisum0lem1b  27482  dchrisum0lem1  27483  dchrisum0lem2a  27484  dchrisum0lem2  27485  dchrisum0lem3  27486  dchrisum0  27487  pntlem3  27576  axcontlem2  29038  axcontlem7  29043  axcontlem8  29044  axcontlem10  29046  upgrreslem  29377  umgrreslem  29378  usgrres  29381  vtxdginducedm1lem2  29614  finsumvtxdg2ssteplem1  29619  clwwlksswrd  30062  frgrwopregbsn  30392  frgrwopreg1  30393  atssch  32418  partfun2  32755  fcobijfs  32800  fcobijfs2  32801  elrgspnlem1  33324  elrgspnlem2  33325  nsgmgc  33493  ssdifidllem  33537  ssdifidlprm  33539  ssmxidllem  33554  1arithufdlem2  33626  1arithufdlem4  33628  extvfvvcl  33700  mplmulmvr  33704  esplymhp  33726  esplyfv1  33727  esplysply  33729  esplyfval3  33730  esplyind  33731  eulerpartlemgvv  34533  reprpmtf1o  34783  hgt750lemb  34813  hgt750leme  34815  bnj1212  34955  bnj213  35038  bnj1286  35175  bnj1312  35214  bnj1523  35227  subfacp1lem3  35376  subfacp1lem5  35378  wlimss  36021  bj-smgrpssmgm  37473  bj-mndsssmgrp  37475  bj-cmnssmnd  37477  bj-grpssmnd  37479  aks6d1c6lem4  42427  readvcot  42619  evlsmhpvvval  42838  fglmod  43315  naddwordnexlem4  43643  scottss  44484  limcperiod  45874  cncfshift  46118  cncfperiod  46123  ovnsslelem  46804  ovolval5lem3  46898  uspgrlimlem2  48235  uspgrlim  48238