Theorem ssrab3 4044

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

Syntax hints:   = wceq 1567  {crab 3423   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-ss 3930

This theorem is referenced by:  dmmptss  6243  omsson  7866  oawordeulem  8539  ordtypelem2  9481  wemapso2lem  9514  wemapwe  9666  scottss  9869  cplem1  9875  cofsmo  10253  fin23lem28  10324  fin23lem30  10326  isf32lem5  10341  isf32lem6  10342  isf32lem7  10343  isf32lem8  10344  hsmexlem4  10413  hsmexlem5  10414  hsmexlem6  10415  zorn2lem1  10480  zorn2lem3  10482  zorn2lem4  10483  zorn2lem5  10484  0nnq  10909  elpqn  10910  rpnnen1lem2  13001  rpssre  13024  01sqrexlem5  15297  dvdsflip  16375  divalglem2  16453  divalglem5  16455  divalglem8  16458  gcdcllem3  16559  bezoutlem2  16598  bezoutlem3  16599  maxprmfct  16768  phimullem  16838  eulerthlem2  16841  pclem  16898  infpn2  16973  prmreclem2  16977  prmreclem3  16978  prmreclem5  16980  4sqlem13  17017  4sqlem14  17018  4sqlem17  17021  4sqlem18  17022  vdwnnlem3  17057  ramcl2lem  17069  ramtcl  17070  ramtcl2  17071  ramtub  17072  imasdsval2  17570  gsumval1  18741  nmzsubg  19231  nmznsg  19234  conjnmz  19322  conjnmzb  19323  gastacl  19379  sylow1lem2  19669  sylow1lem3  19670  sylow1lem4  19671  sylow1lem5  19672  sylow2a  19689  sylow3lem2  19698  ablfacrplem  20137  ablfacrp2  20139  ablfac1eu  20145  pgpfaclem1  20153  ablfaclem2  20158  ablfaclem3  20159  nzrring  20599  lringnzr  20626  rrgeq0  20785  rrgss  20787  lspsolvlem  21244  lbsextlem2  21261  lbsextlem3  21262  lbsextlem4  21263  ssdifidllem  21453  ssdifidlprm  21455  cygznlem2a  21686  psgnghm  21699  dsmmbase  21854  frlmsslsp  21915  psrbagconf1o  22048  psrass1lem  22052  mplbasss  22115  coe1mul2lem2  22398  mretopd  23218  hauscmplem  23532  ptcmplem1  24178  ptcmplem3  24180  tgpconncompeqg  24238  imasdsf1olem  24499  blcld  24631  icccmplem1  24949  icccmplem2  24950  icccmplem3  24951  rrxf  25529  ivthlem1  25579  ivthlem2  25580  ivthlem3  25581  ovolsslem  25612  ovolicc2lem3  25647  ovolicc2lem4  25648  ovolicc2lem5  25649  ovolicc2  25650  dyadmbllem  25727  dyadmbl  25728  iblmbf  25895  abelthlem4  26563  abelthlem6  26565  abelthlem9  26569  abelth  26570  dvatan  27066  atancn  27067  lgamucov  27168  lgamucov2  27169  ftalem3  27205  mpodvdsmulf1o  27324  fsumdvdsmul  27325  dvdsmulf1o  27326  lgsfcl2  27433  rpvmasum2  27642  dchrisum0re  27643  dchrisum0lema  27644  dchrisum0lem1b  27645  dchrisum0lem1  27646  dchrisum0lem2a  27647  dchrisum0lem2  27648  dchrisum0lem3  27649  dchrisum0  27650  pntlem3  27739  axcontlem2  29256  axcontlem7  29261  axcontlem8  29262  axcontlem10  29264  upgrreslem  29595  umgrreslem  29596  usgrres  29599  vtxdginducedm1lem2  29831  finsumvtxdg2ssteplem1  29836  clwwlksswrd  30279  frgrwopregbsn  30609  frgrwopreg1  30610  atssch  32636  partfun2  32962  fcobijfs  33007  fcobijfs2  33008  elrgspnlem1  33503  elrgspnlem2  33504  nsgmgc  33665  ssmxidllem  33701  1arithufdlem2  33780  1arithufdlem4  33782  extvfvvcl  33870  mplmulmvr  33874  psrmonprod  33887  esplymhp  33903  esplyfv1  33904  esplysply  33906  esplyfval3  33907  esplyind  33910  eulerpartlemgvv  34711  reprpmtf1o  34958  hgt750lemb  34988  hgt750leme  34990  bnj1212  35132  bnj213  35215  bnj1286  35352  bnj1312  35391  bnj1523  35404  subfacp1lem3  35607  subfacp1lem5  35609  wlimss  36252  bj-smgrpssmgm  37834  bj-mndsssmgrp  37836  bj-cmnssmnd  37838  bj-grpssmnd  37840  aks6d1c6lem4  42864  readvcot  43049  evlsmhpvvval  43253  fglmod  43726  naddwordnexlem4  44054  limcperiod  46270  cncfshift  46514  cncfperiod  46519  ovnsslelem  47200  ovolval5lem3  47294  uspgrlimlem2  48677  uspgrlim  48680