Theorem ssrab3 4030

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

This proof depends on syntax axioms:   = wceq 1570  {crab 3413   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-ss 3916

This theorem is used by:  dmmptss  6235  omsson  7870  oawordeulem  8546  ordtypelem2  9497  wemapso2lem  9530  wemapwe  9682  scottss  9916  cplem1OLD  9932  cofsmo  10328  fin23lem28  10399  fin23lem30  10401  isf32lem5  10416  isf32lem6  10417  isf32lem7  10418  isf32lem8  10419  hsmexlem4  10488  hsmexlem5  10489  hsmexlem6  10490  zorn2lem1  10555  zorn2lem3  10557  zorn2lem4  10558  zorn2lem5  10559  0nnq  10990  elpqn  10991  rpnnen1lem2  13086  rpssre  13109  01sqrexlem5  15393  dvdsflip  16467  divalglem2  16545  divalglem5  16547  divalglem8  16550  gcdcllem3  16651  bezoutlem2  16693  bezoutlem3  16694  maxprmfct  16865  phimullem  16936  eulerthlem2  16939  pclem  16996  infpn2  17071  prmreclem2  17075  prmreclem3  17076  prmreclem5  17078  4sqlem13  17115  4sqlem14  17116  4sqlem17  17119  4sqlem18  17120  vdwnnlem3  17155  ramcl2lem  17167  ramtcl  17168  ramtcl2  17169  ramtub  17170  imasdsval2  17668  gsumval1  18852  nmzsubg  19355  nmznsg  19358  conjnmz  19446  conjnmzb  19447  gastacl  19503  sylow1lem2  19793  sylow1lem3  19794  sylow1lem4  19795  sylow1lem5  19796  sylow2a  19813  sylow3lem2  19822  ablfacrplem  20261  ablfacrp2  20263  ablfac1eu  20269  pgpfaclem1  20277  ablfaclem2  20282  ablfaclem3  20283  nzrring  20746  lringnzr  20773  rrgeq0  20932  rrgss  20934  lspsolvlem  21400  lbsextlem2  21417  lbsextlem3  21418  lbsextlem4  21419  ssdifidllem  21620  ssdifidlprm  21622  cygznlem2a  21853  psgnghm  21866  dsmmbase  22021  frlmsslsp  22082  psrbagconf1o  22217  psrass1lem  22221  mplbasss  22284  coe1mul2lem2  22567  mretopd  23390  hauscmplem  23704  ptcmplem1  24351  ptcmplem3  24353  tgpconncompeqg  24411  imasdsf1olem  24672  blcld  24804  icccmplem1  25122  icccmplem2  25123  icccmplem3  25124  rrxf  25702  ivthlem1  25752  ivthlem2  25753  ivthlem3  25754  ovolsslem  25785  ovolicc2lem3  25820  ovolicc2lem4  25821  ovolicc2lem5  25822  ovolicc2  25823  dyadmbllem  25900  dyadmbl  25901  iblmbf  26068  abelthlem4  26743  abelthlem6  26745  abelthlem9  26749  abelth  26750  dvatan  27245  atancn  27246  lgamucov  27347  lgamucov2  27348  ftalem3  27384  mpodvdsmulf1o  27503  fsumdvdsmul  27504  dvdsmulf1o  27505  lgsfcl2  27612  rpvmasum2  27821  dchrisum0re  27822  dchrisum0lema  27823  dchrisum0lem1b  27824  dchrisum0lem1  27825  dchrisum0lem2a  27826  dchrisum0lem2  27827  dchrisum0lem3  27828  dchrisum0  27829  pntlem3  27918  elcgrabasi  29357  axcontlem2  29525  axcontlem7  29530  axcontlem8  29531  axcontlem10  29533  upgrreslem  29867  umgrreslem  29868  usgrres  29871  vtxdginducedm1lem2  30103  finsumvtxdg2ssteplem1  30108  clwwlksswrd  30560  frgrwopregbsn  30900  frgrwopreg1  30901  atssch  32927  partfun2  33252  fcobijfs  33295  fcobijfs2  33296  elrgspnlem1  33785  elrgspnlem2  33786  nsgmgc  33945  ssmxidllem  33980  1arithufdlem2  34059  1arithufdlem4  34061  extvfvvcl  34149  mplmulmvr  34153  psrmonprod  34166  esplymhp  34182  esplyfv1  34183  esplysply  34185  esplyfval3  34186  esplyind  34189  eulerpartlemgvv  34991  reprpmtf1o  35238  hgt750lemb  35268  hgt750leme  35270  bnj1212  35412  bnj213  35495  bnj1286  35632  bnj1312  35671  bnj1523  35684  subfacp1lem3  35916  subfacp1lem5  35918  wlimss  36561  bj-smgrpssmgm  38157  bj-mndsssmgrp  38159  bj-cmnssmnd  38161  bj-grpssmnd  38163  aks6d1c6lem4  43191  readvcot  43383  evlsmhpvvval  43585  fglmod  44033  naddwordnexlem4  44361  limcperiod  46584  cncfshift  46828  cncfperiod  46833  ovnsslelem  47514  ovolval5lem3  47608  uspgrlimlem2  49031  uspgrlim  49034