Theorem ssrab3 4057

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

Syntax hints:   = wceq 1540  {crab 3415   ⊆ wss 3926

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-ss 3943

This theorem is referenced by:  dmmptss  6230  omsson  7863  oawordeulem  8564  ordtypelem2  9531  wemapso2lem  9564  wemapwe  9709  cplem1  9901  cofsmo  10281  fin23lem28  10352  fin23lem30  10354  isf32lem5  10369  isf32lem6  10370  isf32lem7  10371  isf32lem8  10372  hsmexlem4  10441  hsmexlem5  10442  hsmexlem6  10443  zorn2lem1  10508  zorn2lem3  10510  zorn2lem4  10511  zorn2lem5  10512  0nnq  10936  elpqn  10937  rpnnen1lem2  12991  rpssre  13014  01sqrexlem5  15263  dvdsflip  16334  divalglem2  16412  divalglem5  16414  divalglem8  16417  gcdcllem3  16518  bezoutlem2  16557  bezoutlem3  16558  maxprmfct  16726  phimullem  16796  eulerthlem2  16799  pclem  16856  infpn2  16931  prmreclem2  16935  prmreclem3  16936  prmreclem5  16938  4sqlem13  16975  4sqlem14  16976  4sqlem17  16979  4sqlem18  16980  vdwnnlem3  17015  ramcl2lem  17027  ramtcl  17028  ramtcl2  17029  ramtub  17030  imasdsval2  17528  gsumval1  18659  nmzsubg  19146  nmznsg  19149  conjnmz  19233  conjnmzb  19234  gastacl  19290  sylow1lem2  19578  sylow1lem3  19579  sylow1lem4  19580  sylow1lem5  19581  sylow2a  19598  sylow3lem2  19607  ablfacrplem  20046  ablfacrp2  20048  ablfac1eu  20054  pgpfaclem1  20062  ablfaclem2  20067  ablfaclem3  20068  nzrring  20474  lringnzr  20499  rrgeq0  20658  rrgss  20660  lspsolvlem  21101  lbsextlem2  21118  lbsextlem3  21119  lbsextlem4  21120  cygznlem2a  21526  psgnghm  21538  dsmmbase  21693  frlmsslsp  21754  psrbagconf1o  21887  psrass1lem  21890  mplbasss  21955  coe1mul2lem2  22203  mretopd  23028  hauscmplem  23342  ptcmplem1  23988  ptcmplem3  23990  tgpconncompeqg  24048  imasdsf1olem  24310  blcld  24442  icccmplem1  24760  icccmplem2  24761  icccmplem3  24762  rrxf  25351  ivthlem1  25402  ivthlem2  25403  ivthlem3  25404  ovolsslem  25435  ovolicc2lem3  25470  ovolicc2lem4  25471  ovolicc2lem5  25472  ovolicc2  25473  dyadmbllem  25550  dyadmbl  25551  iblmbf  25718  abelthlem4  26394  abelthlem6  26396  abelthlem9  26400  abelth  26401  dvatan  26895  atancn  26896  lgamucov  26998  lgamucov2  26999  ftalem3  27035  mpodvdsmulf1o  27154  fsumdvdsmul  27155  dvdsmulf1o  27156  fsumdvdsmulOLD  27157  lgsfcl2  27264  rpvmasum2  27473  dchrisum0re  27474  dchrisum0lema  27475  dchrisum0lem1b  27476  dchrisum0lem1  27477  dchrisum0lem2a  27478  dchrisum0lem2  27479  dchrisum0lem3  27480  dchrisum0  27481  pntlem3  27570  axcontlem2  28890  axcontlem7  28895  axcontlem8  28896  axcontlem10  28898  upgrreslem  29229  umgrreslem  29230  usgrres  29233  vtxdginducedm1lem2  29466  finsumvtxdg2ssteplem1  29471  clwwlksswrd  29914  frgrwopregbsn  30244  frgrwopreg1  30245  atssch  32270  fcobijfs  32646  elrgspnlem1  33183  elrgspnlem2  33184  nsgmgc  33373  ssdifidllem  33417  ssdifidlprm  33419  ssmxidllem  33434  1arithufdlem2  33506  1arithufdlem4  33508  eulerpartlemgvv  34354  reprpmtf1o  34604  hgt750lemb  34634  hgt750leme  34636  bnj1212  34776  bnj213  34859  bnj1286  34996  bnj1312  35035  bnj1523  35048  subfacp1lem3  35150  subfacp1lem5  35152  wlimss  35793  bj-smgrpssmgm  37232  bj-mndsssmgrp  37234  bj-cmnssmnd  37236  bj-grpssmnd  37238  aks6d1c6lem4  42132  readvcot  42354  evlsmhpvvval  42565  fglmod  43044  naddwordnexlem4  43372  scottss  44215  limcperiod  45605  cncfshift  45851  cncfperiod  45856  ovnsslelem  46537  ovolval5lem3  46631  uspgrlimlem2  47949  uspgrlim  47952