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 4011	1 ⊢ 𝐵 ⊆ 𝐴

Syntax hints:   = wceq 1533  {crab 3418   ⊆ wss 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3419  df-ss 3961

This theorem is referenced by:  dmmptss  6247  omsson  7875  oawordeulem  8575  ordtypelem2  9544  wemapso2lem  9577  wemapwe  9722  cplem1  9914  cofsmo  10294  fin23lem28  10365  fin23lem30  10367  isf32lem5  10382  isf32lem6  10383  isf32lem7  10384  isf32lem8  10385  hsmexlem4  10454  hsmexlem5  10455  hsmexlem6  10456  zorn2lem1  10521  zorn2lem3  10523  zorn2lem4  10524  zorn2lem5  10525  0nnq  10949  elpqn  10950  rpnnen1lem2  12994  rpssre  13016  01sqrexlem5  15229  dvdsflip  16297  divalglem2  16375  divalglem5  16377  divalglem8  16380  gcdcllem3  16479  bezoutlem2  16519  bezoutlem3  16520  maxprmfct  16683  phimullem  16751  eulerthlem2  16754  pclem  16810  infpn2  16885  prmreclem2  16889  prmreclem3  16890  prmreclem5  16892  4sqlem13  16929  4sqlem14  16930  4sqlem17  16933  4sqlem18  16934  vdwnnlem3  16969  ramcl2lem  16981  ramtcl  16982  ramtcl2  16983  ramtub  16984  imasdsval2  17501  gsumval1  18646  nmzsubg  19128  nmznsg  19131  conjnmz  19215  conjnmzb  19216  gastacl  19272  sylow1lem2  19566  sylow1lem3  19567  sylow1lem4  19568  sylow1lem5  19569  sylow2a  19586  sylow3lem2  19595  ablfacrplem  20034  ablfacrp2  20036  ablfac1eu  20042  pgpfaclem1  20050  ablfaclem2  20055  ablfaclem3  20056  nzrring  20467  lringnzr  20490  lspsolvlem  21042  lbsextlem2  21059  lbsextlem3  21060  lbsextlem4  21061  rrgeq0  21254  rrgss  21256  cygznlem2a  21518  psgnghm  21529  dsmmbase  21686  frlmsslsp  21747  psrbagconf1o  21887  psrbagconf1oOLD  21888  psrass1lemOLD  21891  psrass1lem  21894  mplbasss  21959  coe1mul2lem2  22212  mretopd  23040  hauscmplem  23354  ptcmplem1  24000  ptcmplem3  24002  tgpconncompeqg  24060  imasdsf1olem  24323  blcld  24458  icccmplem1  24782  icccmplem2  24783  icccmplem3  24784  rrxf  25373  ivthlem1  25424  ivthlem2  25425  ivthlem3  25426  ovolsslem  25457  ovolicc2lem3  25492  ovolicc2lem4  25493  ovolicc2lem5  25494  ovolicc2  25495  dyadmbllem  25572  dyadmbl  25573  iblmbf  25741  abelthlem4  26416  abelthlem6  26418  abelthlem9  26422  abelth  26423  dvatan  26912  atancn  26913  lgamucov  27015  lgamucov2  27016  ftalem3  27052  mpodvdsmulf1o  27171  fsumdvdsmul  27172  dvdsmulf1o  27173  fsumdvdsmulOLD  27174  lgsfcl2  27281  rpvmasum2  27490  dchrisum0re  27491  dchrisum0lema  27492  dchrisum0lem1b  27493  dchrisum0lem1  27494  dchrisum0lem2a  27495  dchrisum0lem2  27496  dchrisum0lem3  27497  dchrisum0  27498  pntlem3  27587  axcontlem2  28848  axcontlem7  28853  axcontlem8  28854  axcontlem10  28856  upgrreslem  29189  umgrreslem  29190  usgrres  29193  vtxdginducedm1lem2  29426  finsumvtxdg2ssteplem1  29431  clwwlksswrd  29869  frgrwopregbsn  30199  frgrwopreg1  30200  atssch  32225  fcobijfs  32587  nsgmgc  33224  ssdifidllem  33268  ssdifidlprm  33270  ssmxidllem  33285  1arithufdlem2  33357  1arithufdlem4  33359  eulerpartlemgvv  34124  reprpmtf1o  34386  hgt750lemb  34416  hgt750leme  34418  bnj1212  34558  bnj213  34641  bnj1286  34778  bnj1312  34817  bnj1523  34830  subfacp1lem3  34920  subfacp1lem5  34922  wlimss  35553  bj-smgrpssmgm  36875  bj-mndsssmgrp  36877  bj-cmnssmnd  36879  bj-grpssmnd  36881  aks6d1c6lem4  41773  evlsmhpvvval  41960  fglmod  42636  naddwordnexlem4  42970  scottss  43819  limcperiod  45151  cncfshift  45397  cncfperiod  45402  ovnsslelem  46083  ovolval5lem3  46177