Theorem ssrab3 4048

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

Syntax hints:   = wceq 1540  {crab 3408   ⊆ wss 3917

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-ss 3934

This theorem is referenced by:  dmmptss  6217  omsson  7849  oawordeulem  8521  ordtypelem2  9479  wemapso2lem  9512  wemapwe  9657  cplem1  9849  cofsmo  10229  fin23lem28  10300  fin23lem30  10302  isf32lem5  10317  isf32lem6  10318  isf32lem7  10319  isf32lem8  10320  hsmexlem4  10389  hsmexlem5  10390  hsmexlem6  10391  zorn2lem1  10456  zorn2lem3  10458  zorn2lem4  10459  zorn2lem5  10460  0nnq  10884  elpqn  10885  rpnnen1lem2  12943  rpssre  12966  01sqrexlem5  15219  dvdsflip  16294  divalglem2  16372  divalglem5  16374  divalglem8  16377  gcdcllem3  16478  bezoutlem2  16517  bezoutlem3  16518  maxprmfct  16686  phimullem  16756  eulerthlem2  16759  pclem  16816  infpn2  16891  prmreclem2  16895  prmreclem3  16896  prmreclem5  16898  4sqlem13  16935  4sqlem14  16936  4sqlem17  16939  4sqlem18  16940  vdwnnlem3  16975  ramcl2lem  16987  ramtcl  16988  ramtcl2  16989  ramtub  16990  imasdsval2  17486  gsumval1  18617  nmzsubg  19104  nmznsg  19107  conjnmz  19191  conjnmzb  19192  gastacl  19248  sylow1lem2  19536  sylow1lem3  19537  sylow1lem4  19538  sylow1lem5  19539  sylow2a  19556  sylow3lem2  19565  ablfacrplem  20004  ablfacrp2  20006  ablfac1eu  20012  pgpfaclem1  20020  ablfaclem2  20025  ablfaclem3  20026  nzrring  20432  lringnzr  20457  rrgeq0  20616  rrgss  20618  lspsolvlem  21059  lbsextlem2  21076  lbsextlem3  21077  lbsextlem4  21078  cygznlem2a  21484  psgnghm  21496  dsmmbase  21651  frlmsslsp  21712  psrbagconf1o  21845  psrass1lem  21848  mplbasss  21913  coe1mul2lem2  22161  mretopd  22986  hauscmplem  23300  ptcmplem1  23946  ptcmplem3  23948  tgpconncompeqg  24006  imasdsf1olem  24268  blcld  24400  icccmplem1  24718  icccmplem2  24719  icccmplem3  24720  rrxf  25308  ivthlem1  25359  ivthlem2  25360  ivthlem3  25361  ovolsslem  25392  ovolicc2lem3  25427  ovolicc2lem4  25428  ovolicc2lem5  25429  ovolicc2  25430  dyadmbllem  25507  dyadmbl  25508  iblmbf  25675  abelthlem4  26351  abelthlem6  26353  abelthlem9  26357  abelth  26358  dvatan  26852  atancn  26853  lgamucov  26955  lgamucov2  26956  ftalem3  26992  mpodvdsmulf1o  27111  fsumdvdsmul  27112  dvdsmulf1o  27113  fsumdvdsmulOLD  27114  lgsfcl2  27221  rpvmasum2  27430  dchrisum0re  27431  dchrisum0lema  27432  dchrisum0lem1b  27433  dchrisum0lem1  27434  dchrisum0lem2a  27435  dchrisum0lem2  27436  dchrisum0lem3  27437  dchrisum0  27438  pntlem3  27527  axcontlem2  28899  axcontlem7  28904  axcontlem8  28905  axcontlem10  28907  upgrreslem  29238  umgrreslem  29239  usgrres  29242  vtxdginducedm1lem2  29475  finsumvtxdg2ssteplem1  29480  clwwlksswrd  29923  frgrwopregbsn  30253  frgrwopreg1  30254  atssch  32279  fcobijfs  32653  elrgspnlem1  33200  elrgspnlem2  33201  nsgmgc  33390  ssdifidllem  33434  ssdifidlprm  33436  ssmxidllem  33451  1arithufdlem2  33523  1arithufdlem4  33525  eulerpartlemgvv  34374  reprpmtf1o  34624  hgt750lemb  34654  hgt750leme  34656  bnj1212  34796  bnj213  34879  bnj1286  35016  bnj1312  35055  bnj1523  35068  subfacp1lem3  35176  subfacp1lem5  35178  wlimss  35824  bj-smgrpssmgm  37263  bj-mndsssmgrp  37265  bj-cmnssmnd  37267  bj-grpssmnd  37269  aks6d1c6lem4  42168  readvcot  42359  evlsmhpvvval  42590  fglmod  43069  naddwordnexlem4  43397  scottss  44239  limcperiod  45633  cncfshift  45879  cncfperiod  45884  ovnsslelem  46565  ovolval5lem3  46659  uspgrlimlem2  47992  uspgrlim  47995