Theorem ssrab2 4021

Description: Subclass relation for a restricted class. (Contributed by NM, 19-Mar-1997.) (Proof shortened by BJ and SN, 8-Aug-2024.)

Assertion

Ref	Expression
ssrab2	⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem ssrab2

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elrabi 3631	. 2 ⊢ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} → 𝑦 ∈ 𝐴)
2	1	ssriv 3926	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴

Syntax hints:  {crab 3390   ⊆ wss 3890

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-ss 3907

This theorem is referenced by:  ssrab3  4023  ssrabeq  4025  iinrab2  5013  riinrab  5027  rabelpw  5273  rabexgOLD  5275  frminex  5603  wereu2  5621  predres  6297  frpomin  6298  frpoinsg  6301  ssimaex  6919  f1oresrab  7074  weniso  7302  canth  7314  riotacl  7334  riotassuni  7357  onminesb  7740  onminsb  7741  onintrab  7743  onnminsb  7746  onminex  7749  tfisg  7798  tfis  7799  suppssdm  8120  fnsuppres  8134  oeeulem  8530  nnawordex  8566  pmvalg  8777  fineqvlem  9169  ordtypelem3  9428  ordtypelem4  9429  ordtypelem6  9431  hartogs  9452  card2on  9462  wdom2d  9488  oemapvali  9596  frinsg  9666  tz9.12lem1  9702  tz9.12lem3  9704  rankf  9709  cardf2  9858  cardid2  9868  cardmin2  9914  acni3  9960  dfac2a  10043  cofsmo  10182  coftr  10186  fin2i2  10231  isfin2-2  10232  enfin2i  10234  fin1a2lem11  10323  fin1a2lem12  10324  axdc3lem4  10366  ac6  10393  ondomon  10476  alephval2  10486  pwfseqlem1  10572  pwfseqlem3  10574  wunccl  10658  tskmcl  10755  infm3  12106  uzf  12782  nnwos  12856  supminf  12876  zsupss  12878  rpnnen1lem1  12919  rpnnen1lem3  12920  rpnnen1lem5  12922  ixxf  13299  fzf  13456  flval3  13765  rabssnn0fi  13939  expge0  14051  expge1  14052  hashbclem  14405  01sqrexlem3  15197  rlimrege0  15532  incexc2  15794  bitsf  16387  bitsfzolem  16394  sadadd2lem  16419  sadadd3  16421  sadcl  16422  smupf  16438  smuval2  16442  smupvallem  16443  smucl  16444  smueqlem  16450  lcmcllem  16556  lcmn0cl  16557  lcmledvds  16559  lcmfval  16581  lcmfcllem  16585  lcmfn0cl  16586  lcmfledvds  16592  phicl2  16729  phibnd  16732  hashdvds  16736  phiprmpw  16737  phimullem  16740  eulerth  16744  phisum  16752  odzcllem  16754  odzdvds  16757  prmreclem1  16878  prmreclem2  16879  prmreclem3  16880  prmreclem4  16881  prmreclem5  16882  hashbccl  16965  prmgaplem3  17015  prmgaplem4  17016  prdsds  17418  mrcflem  17563  isacs1i  17614  wunnat  17917  dmcoass  18024  lublecl  18316  lubid  18317  rabsubmgmd  18663  mgmhmeql  18675  issubmd  18765  mhmeql  18785  cntzval  19287  cntzssv  19294  symgsssg  19433  symgfisg  19434  pmtrdifellem4  19445  odfval  19498  odlem1  19501  odlem2  19505  odngen  19543  gexlem1  19545  gexlem2  19548  sylow2alem2  19584  sylow2blem3  19588  oddvdssubg  19821  cyggex2  19863  ablfaclem3  20055  rgspncl  20581  lssacs  20953  lspf  20960  ocvfval  21656  ocvval  21657  dsmmval2  21726  dsmmsubg  21733  asplss  21863  aspsubrg  21865  psrass1lem  21922  psrdi  21953  psrdir  21954  psrass23l  21955  psrass23  21957  resspsrmul  21964  mplbas  21978  mplsubglem  21987  mplsubrglem  21992  mplmonmul  22024  psropprmul  22211  scmatlss  22500  smadiadet  22645  pmatcoe1fsupp  22676  cpmatsubgpmat  22695  fctop  22979  cctop  22981  ppttop  22982  epttop  22984  clscld  23022  neips  23088  neiptopnei  23107  ordtbaslem  23163  ordtuni  23165  ordtcld1  23172  ordtcld2  23173  cnpfval  23209  iscnp2  23214  cmpcov2  23365  cmpsublem  23374  tgcmp  23376  conncompcld  23409  1stcfb  23420  2ndc1stc  23426  2ndcdisj  23431  finlocfin  23495  kgentopon  23513  xkotf  23560  txkgen  23627  xkococnlem  23634  imastopn  23695  kqffn  23700  opnfbas  23817  flimfnfcls  24003  alexsubALT  24026  ptcmplem2  24028  symgtgp  24081  tgpconncompeqg  24087  tgpconncomp  24088  ghmcnp  24090  tsmsfbas  24103  eltsms  24108  utoptop  24209  utopbas  24210  blfvalps  24358  blfps  24381  blf  24382  nmoffn  24686  nmofval  24689  nmogelb  24691  nmolb  24692  nmof  24694  ishtpy  24949  clsocv  25227  rrxnm  25368  rrxbasefi  25387  minveclem3b  25405  minveclem4  25409  ovolcl  25455  ovollb  25456  ovolgelb  25457  ovolge0  25458  ovolshftlem1  25486  ovolshft  25488  ovolscalem1  25490  ovolscalem2  25491  ovolsca  25492  ovolicc2lem3  25496  shftmbl  25515  iundisj  25525  dyadmax  25575  dyadmbllem  25576  opnmbllem  25578  mdegmullem  26053  uc1pval  26115  mon1pval  26117  elqaalem1  26296  elqaalem3  26298  aannenlem2  26306  aalioulem2  26310  radcnvcl  26395  radcnvlt1  26396  radcnvle  26398  ftalem4  27053  ftalem5  27054  efnnfsumcl  27080  isppw  27091  sgmval2  27120  efchtdvds  27136  sqff1o  27159  fsumdvdsdiaglem  27160  fsumdvdsdiag  27161  fsumdvdscom  27162  musum  27168  muinv  27170  sgmmul  27178  ppiub  27181  vmasum  27193  logfac2  27194  perfectlem2  27207  lgsfcl  27282  lgscl  27288  lgsquadlem1  27357  lgsquadlem2  27358  rpvmasumlem  27464  mudivsum  27507  mulogsum  27509  mulog2sumlem2  27512  vmalogdivsum2  27515  logsqvma  27519  logsqvma2  27520  selberglem3  27524  selberg  27525  selberg34r  27548  pntsval2  27553  pntrlog2bndlem1  27554  ltsval2  27634  conway  27785  eqcuts2  27792  cutsun12  27796  cutbdaybnd  27801  cutbdaybnd2  27802  cutbdaylt  27804  bday1  27820  cuteq0  27821  madef  27842  leftssold  27877  rightssold  27878  madebdaylemlrcut  27905  sltsbday  27923  cofcut1  27926  cofcutr  27930  cutlt  27938  precsexlem8  28220  precsexlem11  28223  onssno  28260  oncutlt  28270  oniso  28277  bdayons  28282  bdayn0p1  28375  tglnunirn  28630  tglnssp  28634  incistruhgr  29162  upgrss  29171  upgrn0  29172  upgruhgr  29185  usgrss  29257  uspgrushgr  29260  ushgredgedg  29312  ushgredgedgloop  29314  vtxdun  29565  vtxdginducedm1  29627  wlknwwlksnbij  29971  hashwwlksnext  29997  frcond3  30354  numclwlk1lem2  30455  ocsh  31369  spancl  31422  shsval2i  31473  ococin  31494  chsupid  31498  speccl  31985  hatomistici  32448  chpssati  32449  iundisjf  32674  aciunf1  32751  fpwrelmap  32821  iundisjfi  32884  pwrssmgc  33075  cycpmco2f1  33200  cycpmco2rn  33201  cycpmco2lem1  33202  cycpmco2lem2  33203  cycpmco2lem3  33204  cycpmco2lem4  33205  cycpmco2lem5  33206  cycpmco2lem6  33207  cycpmco2lem7  33208  cycpmco2  33209  fxpss  33242  nsgmgclem  33486  extvfvcl  33695  mplmulmvr  33698  evlextv  33701  mplvrpmlem  33702  mplvrpmga  33704  mplvrpmrhm  33706  psrmonmul  33709  esplylem  33725  esplympl  33726  esplymhp  33727  esplyfv1  33728  esplyfv  33729  esplyfval3  33731  esplyfval1  33732  esplyfvaln  33733  constrsuc  33898  locfinreflem  34000  zarclsiin  34031  zarcls  34034  zartopn  34035  esumrnmpt2  34228  esumpinfval  34233  sigagensiga  34301  ldgenpisyslem1  34323  ldgenpisys  34326  measvuni  34374  imambfm  34422  dya2iocuni  34443  omscl  34455  oms0  34457  omsmon  34458  omssubadd  34460  carsgcl  34464  oddpwdc  34514  eulerpartlem1  34527  eulerpartlemt  34531  eulerpartgbij  34532  eulerpartlemmf  34535  eulerpartlemgh  34538  eulerpartlemgs2  34540  ballotlem2  34649  ballotlemfc0  34653  ballotlemfcc  34654  ballotlemfmpn  34655  ballotlemiex  34662  ballotlemsup  34665  ballotlem7  34696  ballotth  34698  reprpmtf1o  34786  breprexplema  34790  hgt750lema  34817  bnj110  35016  bnj1204  35170  bnj1311  35182  fnrelpredd  35250  subfacp1lem6  35383  erdszelem2  35390  connpconn  35433  cvmliftmolem2  35480  cvmliftlem15  35496  cvmlift2lem12  35512  snmlff  35527  satfrnmapom  35568  rankeq1o  36369  finminlem  36516  fnessref  36555  neibastop1  36557  neibastop2lem  36558  weiunlem  36661  weiunse  36666  bj-rabtr  37253  bj-rabtrAUTO  37255  bj-vecssmod  37611  icoreresf  37682  phpreu  37939  fin2so  37942  poimirlem26  37981  poimirlem31  37986  poimirlem32  37987  opnmbllem0  37991  mblfinlem1  37992  mblfinlem2  37993  ismblfin  37996  mbfposadd  38002  cnambfre  38003  cover2  38050  indexa  38068  fdc  38080  sstotbnd2  38109  sstotbnd3  38111  igenidl  38398  prnc  38402  toycom  39433  lkrlss  39555  atlatmstc  39779  atlatle  39780  glbconN  39837  linepsubN  40212  pmapssat  40219  pmaple  40221  pmapsub  40228  paddssat  40274  diass  41502  diaglbN  41515  diaintclN  41518  diassdvaN  41520  docaclN  41584  dibglbN  41626  dibintclN  41627  diclspsn  41654  dihglblem2N  41754  dih1dimatlem  41789  dihglb2  41802  dochval2  41812  dochcl  41813  dochvalr  41817  doch2val2  41824  dochss  41825  dochocss  41826  lclkr  41993  lclkrs  41999  lcdvbase  42053  lcdvbasess  42054  mapdunirnN  42110  aks4d1p4  42532  aks4d1p5  42533  aks4d1p7  42536  aks4d1p8  42540  sticksstones1  42599  aks6d1c6lem2  42624  grpods  42647  unitscyglem1  42648  unitscyglem2  42649  unitscyglem4  42651  mhpind  43041  mhphf  43044  prjcrv0  43080  infdesc  43090  mzpindd  43192  fiphp3d  43265  rencldnfilem  43266  irrapx1  43274  pellexlem3  43277  pellfundre  43327  pellfundge  43328  pellfundlb  43330  pellfundglb  43331  jm2.22  43441  jm2.23  43442  rpnnen3  43478  pwssplit4  43535  pwfi2f1o  43542  hbtlem6  43575  dgraalem  43591  dgraaub  43594  itgocn  43610  onintunirab  43673  nadd2rabord  43831  nadd1rabord  43835  rfovcnvf1od  44449  fsovfd  44457  fsovcnvlem  44458  binomcxplemdvbinom  44798  binomcxplemcvg  44799  binomcxplemnotnn0  44801  uzwo4  45502  disjf1o  45639  icof  45666  allbutfiinf  45866  supminfxr  45910  supminfxr2  45915  fsumsupp0  46026  sumnnodd  46078  fnlimabslt  46125  liminfvalxr  46229  ioodvbdlimc1lem1  46377  dvnprodlem1  46392  dvnprodlem2  46393  stoweidlem14  46460  stoweidlem34  46480  stoweidlem44  46490  stoweidlem50  46496  stoweidlem51  46497  stoweidlem52  46498  stoweidlem57  46503  stoweidlem59  46505  fourierdlem19  46572  fourierdlem20  46573  fourierdlem25  46578  fourierdlem31  46584  fourierdlem37  46590  fourierdlem42  46595  fourierdlem51  46603  fourierdlem54  46606  fourierdlem64  46616  fourierdlem79  46631  elaa2lem  46679  etransclem16  46696  etransclem24  46704  etransclem31  46711  etransclem33  46713  etransclem34  46714  etransclem48  46728  salgencl  46778  salexct  46780  salgenuni  46783  subsaliuncllem  46803  meadjiunlem  46911  caragenss  46950  caratheodory  46974  ovnlecvr  47004  ovnlerp  47008  ovn0lem  47011  ovnsubaddlem1  47016  hoidmv1lelem1  47037  hoidmv1lelem3  47039  hoidmvlelem1  47041  hoidmvlelem2  47042  hoidmvlelem3  47043  hoidmvlelem4  47044  ovnhoilem1  47047  ovnhoilem2  47048  ovnlecvr2  47056  ovncvr2  47057  opnvonmbllem2  47079  ovolval4lem1  47095  pimconstlt1  47148  pimgtmnf2  47160  pimdecfgtioc  47161  pimincfltioc  47162  pimdecfgtioo  47163  pimincfltioo  47164  sssmf  47184  incsmflem  47187  smfaddlem1  47209  smfaddlem2  47210  decsmflem  47212  smflimlem1  47217  smflimlem2  47218  smflimlem3  47219  smfrec  47235  smfmullem4  47240  smfdiv  47243  smfsuplem1  47257  smfsuplem3  47259  smfinflem  47263  smflimsuplem1  47266  smflimsuplem7  47272  smfliminflem  47276  sprsymrelfolem1  47964  prmdvdsfmtnof1lem1  48059  prmdvdsfmtnof  48061  perfectALTVlem2  48210  isubgredg  48354  isubgruhgr  48356  isubgrgrim  48417  uhgrimisgrgric  48419  uspgrlimlem1  48476  uspgrlimlem4  48479  uspgrlim  48480  grlimgrtrilem2  48490  oddibas  48661  2zlidl  48728  2zrngbas  48730  2zrng0  48732  isclatd  49470  topclat  49485