Theorem ssrab3 4007

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

This proof depends on syntax axioms:   = wceq 1569  {crab 3412   ⊆ wss 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-ss 3896

This theorem is used by:  dmmptss  6242  omsson  7882  oawordeulem  8566  ordtypelem2  9517  wemapso2lem  9550  wemapwe  9702  scottss  9939  cplem1OLD  9955  cofsmo  10351  fin23lem28  10422  fin23lem30  10424  isf32lem5  10439  isf32lem6  10440  isf32lem7  10441  isf32lem8  10442  hsmexlem4  10511  hsmexlem5  10512  hsmexlem6  10513  zorn2lem1  10578  zorn2lem3  10580  zorn2lem4  10581  zorn2lem5  10582  0nnq  11013  elpqn  11014  rpnnen1lem2  13109  rpssre  13132  01sqrexlem5  15419  dvdsflip  16493  divalglem2  16571  divalglem5  16573  divalglem8  16576  gcdcllem3  16677  bezoutlem2  16719  bezoutlem3  16720  maxprmfct  16891  phimullem  16962  eulerthlem2  16965  pclem  17022  infpn2  17097  prmreclem2  17101  prmreclem3  17102  prmreclem5  17104  4sqlem13  17141  4sqlem14  17142  4sqlem17  17145  4sqlem18  17146  vdwnnlem3  17181  ramcl2lem  17193  ramtcl  17194  ramtcl2  17195  ramtub  17196  imasdsval2  17694  gsumval1  18878  nmzsubg  19381  nmznsg  19384  conjnmz  19472  conjnmzb  19473  gastacl  19529  sylow1lem2  19819  sylow1lem3  19820  sylow1lem4  19821  sylow1lem5  19822  sylow2a  19839  sylow3lem2  19848  ablfacrplem  20287  ablfacrp2  20289  ablfac1eu  20295  pgpfaclem1  20303  ablfaclem2  20308  ablfaclem3  20309  nzrring  20772  lringnzr  20799  rrgeq0  20958  rrgss  20960  lspsolvlem  21426  lbsextlem2  21443  lbsextlem3  21444  lbsextlem4  21445  ssdifidllem  21646  ssdifidlprm  21648  cygznlem2a  21879  psgnghm  21892  dsmmbase  22047  frlmsslsp  22108  psrbagconf1o  22243  psrass1lem  22247  mplbasss  22310  coe1mul2lem2  22593  mretopd  23416  hauscmplem  23730  ptcmplem1  24377  ptcmplem3  24379  tgpconncompeqg  24437  imasdsf1olem  24698  blcld  24830  icccmplem1  25148  icccmplem2  25149  icccmplem3  25150  rrxf  25728  ivthlem1  25778  ivthlem2  25779  ivthlem3  25780  ovolsslem  25811  ovolicc2lem3  25846  ovolicc2lem4  25847  ovolicc2lem5  25848  ovolicc2  25849  dyadmbllem  25926  dyadmbl  25927  iblmbf  26094  abelthlem4  26767  abelthlem6  26769  abelthlem9  26773  abelth  26774  dvatan  27269  atancn  27270  lgamucov  27371  lgamucov2  27372  ftalem3  27408  mpodvdsmulf1o  27527  fsumdvdsmul  27528  dvdsmulf1o  27529  lgsfcl2  27636  rpvmasum2  27845  dchrisum0re  27846  dchrisum0lema  27847  dchrisum0lem1b  27848  dchrisum0lem1  27849  dchrisum0lem2a  27850  dchrisum0lem2  27851  dchrisum0lem3  27852  dchrisum0  27853  pntlem3  27942  elcgrabasi  29381  axcontlem2  29549  axcontlem7  29554  axcontlem8  29555  axcontlem10  29557  upgrreslem  29891  umgrreslem  29892  usgrres  29895  vtxdginducedm1lem2  30127  finsumvtxdg2ssteplem1  30132  clwwlksswrd  30584  frgrwopregbsn  30924  frgrwopreg1  30925  atssch  32951  partfun2  33318  fcobijfs  33360  fcobijfs2  33361  elrgspnlem1  33850  elrgspnlem2  33851  nsgmgc  34010  ssmxidllem  34045  1arithufdlem2  34124  1arithufdlem4  34126  extvfvvcl  34214  mplmulmvr  34218  psrmonprod  34231  esplymhp  34247  esplyfv1  34248  esplysply  34250  esplyfval3  34251  esplyind  34254  eulerpartlemgvv  35055  reprpmtf1o  35302  hgt750lemb  35332  hgt750leme  35334  bnj1212  35476  bnj213  35559  bnj1286  35696  bnj1312  35735  bnj1523  35748  subfacp1lem3  36034  subfacp1lem5  36036  wlimss  36684  bj-smgrpssmgm  38283  bj-mndsssmgrp  38285  bj-cmnssmnd  38287  bj-grpssmnd  38289  aks6d1c6lem4  43317  readvcot  43509  evlsmhpvvval  43717  fglmod  44169  naddwordnexlem4  44497  limcperiod  46734  cncfshift  46978  cncfperiod  46983  ovnsslelem  47664  ovolval5lem3  47758  uspgrlimlem2  49181  uspgrlim  49184