Theorem ssrab3 4076

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

Syntax hints:   = wceq 1541  {crab 3431   ⊆ wss 3944

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  df-in 3951  df-ss 3961

This theorem is referenced by:  dmmptss  6229  omsson  7842  oawordeulem  8537  ordtypelem2  9496  wemapso2lem  9529  wemapwe  9674  cplem1  9866  cofsmo  10246  fin23lem28  10317  fin23lem30  10319  isf32lem5  10334  isf32lem6  10335  isf32lem7  10336  isf32lem8  10337  hsmexlem4  10406  hsmexlem5  10407  hsmexlem6  10408  zorn2lem1  10473  zorn2lem3  10475  zorn2lem4  10476  zorn2lem5  10477  0nnq  10901  elpqn  10902  rpnnen1lem2  12943  rpssre  12963  01sqrexlem5  15175  dvdsflip  16242  divalglem2  16320  divalglem5  16322  divalglem8  16325  gcdcllem3  16424  bezoutlem2  16464  bezoutlem3  16465  maxprmfct  16628  phimullem  16694  eulerthlem2  16697  pclem  16753  infpn2  16828  prmreclem2  16832  prmreclem3  16833  prmreclem5  16835  4sqlem13  16872  4sqlem14  16873  4sqlem17  16876  4sqlem18  16877  vdwnnlem3  16912  ramcl2lem  16924  ramtcl  16925  ramtcl2  16926  ramtub  16927  imasdsval2  17444  gsumval1  18584  nmzsubg  19017  nmznsg  19020  conjnmz  19092  conjnmzb  19093  gastacl  19139  sylow1lem2  19431  sylow1lem3  19432  sylow1lem4  19433  sylow1lem5  19434  sylow2a  19451  sylow3lem2  19460  ablfacrplem  19894  ablfacrp2  19896  ablfac1eu  19902  pgpfaclem1  19910  ablfaclem2  19915  ablfaclem3  19916  nzrring  20245  lringnzr  20261  lspsolvlem  20704  lbsextlem2  20721  lbsextlem3  20722  lbsextlem4  20723  rrgeq0  20842  rrgss  20844  cygznlem2a  21056  psgnghm  21066  dsmmbase  21223  frlmsslsp  21284  psrbagconf1o  21420  psrbagconf1oOLD  21421  psrass1lemOLD  21424  psrass1lem  21427  mplbasss  21485  coe1mul2lem2  21721  mretopd  22525  hauscmplem  22839  ptcmplem1  23485  ptcmplem3  23487  tgpconncompeqg  23545  imasdsf1olem  23808  blcld  23943  icccmplem1  24267  icccmplem2  24268  icccmplem3  24269  rrxf  24847  ivthlem1  24897  ivthlem2  24898  ivthlem3  24899  ovolsslem  24930  ovolicc2lem3  24965  ovolicc2lem4  24966  ovolicc2lem5  24967  ovolicc2  24968  dyadmbllem  25045  dyadmbl  25046  iblmbf  25214  abelthlem4  25875  abelthlem6  25877  abelthlem9  25881  abelth  25882  dvatan  26367  atancn  26368  lgamucov  26469  lgamucov2  26470  ftalem3  26506  dvdsmulf1o  26625  fsumdvdsmul  26626  lgsfcl2  26733  rpvmasum2  26942  dchrisum0re  26943  dchrisum0lema  26944  dchrisum0lem1b  26945  dchrisum0lem1  26946  dchrisum0lem2a  26947  dchrisum0lem2  26948  dchrisum0lem3  26949  dchrisum0  26950  pntlem3  27039  axcontlem2  28088  axcontlem7  28093  axcontlem8  28094  axcontlem10  28096  upgrreslem  28426  umgrreslem  28427  usgrres  28430  vtxdginducedm1lem2  28662  finsumvtxdg2ssteplem1  28667  clwwlksswrd  29105  frgrwopregbsn  29435  frgrwopreg1  29436  atssch  31459  fcobijfs  31819  nsgmgc  32379  ssmxidllem  32438  eulerpartlemgvv  33206  reprpmtf1o  33469  hgt750lemb  33499  hgt750leme  33501  bnj1212  33641  bnj213  33724  bnj1286  33861  bnj1312  33900  bnj1523  33913  subfacp1lem3  34004  subfacp1lem5  34006  wlimss  34631  bj-smgrpssmgm  35953  bj-mndsssmgrp  35955  bj-cmnssmnd  35957  bj-grpssmnd  35959  fglmod  41586  naddwordnexlem4  41923  scottss  42773  limcperiod  44117  cncfshift  44363  cncfperiod  44368  ovnsslelem  45049  ovolval5lem3  45143