Theorem ssrab2 4060

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 3670	. 2 ⊢ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} → 𝑦 ∈ 𝐴)
2	1	ssriv 3967	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴

Syntax hints:  {crab 3419   ⊆ wss 3931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3420  df-ss 3948

This theorem is referenced by:  ssrab3  4062  ssrabeq  4064  iinrab2  5050  riinrab  5064  rabelpw  5316  rabexgOLD  5318  frminex  5644  wereu2  5662  predres  6339  frpomin  6340  frpoinsg  6343  wfisgOLD  6354  ssimaex  6974  f1oresrab  7127  weniso  7356  canth  7367  riotacl  7387  riotassuni  7410  onminesb  7795  onminsb  7796  onintrab  7798  onnminsb  7801  onminex  7804  tfisg  7857  tfis  7858  suppssdm  8184  fnsuppres  8198  oeeulem  8621  nnawordex  8657  pmvalg  8859  fineqvlem  9280  ordtypelem3  9542  ordtypelem4  9543  ordtypelem6  9545  hartogs  9566  card2on  9576  wdom2d  9602  oemapvali  9706  frinsg  9773  tz9.12lem1  9809  tz9.12lem3  9811  rankf  9816  cardf2  9965  cardid2  9975  cardmin2  10021  acni3  10069  dfac2a  10152  cofsmo  10291  coftr  10295  fin2i2  10340  isfin2-2  10341  enfin2i  10343  fin1a2lem11  10432  fin1a2lem12  10433  axdc3lem4  10475  ac6  10502  ondomon  10585  alephval2  10594  pwfseqlem1  10680  pwfseqlem3  10682  wunccl  10766  tskmcl  10863  infm3  12209  uzf  12863  nnwos  12939  supminf  12959  zsupss  12961  rpnnen1lem1  13002  rpnnen1lem3  13003  rpnnen1lem5  13005  ixxf  13379  fzf  13533  flval3  13837  rabssnn0fi  14009  expge0  14121  expge1  14122  hashbclem  14473  01sqrexlem3  15265  rlimrege0  15597  incexc2  15856  bitsf  16446  bitsfzolem  16453  sadadd2lem  16478  sadadd3  16480  sadcl  16481  smupf  16497  smuval2  16501  smupvallem  16502  smucl  16503  smueqlem  16509  lcmcllem  16615  lcmn0cl  16616  lcmledvds  16618  lcmfval  16640  lcmfcllem  16644  lcmfn0cl  16645  lcmfledvds  16651  phicl2  16787  phibnd  16790  hashdvds  16794  phiprmpw  16795  phimullem  16798  eulerth  16802  phisum  16810  odzcllem  16812  odzdvds  16815  prmreclem1  16936  prmreclem2  16937  prmreclem3  16938  prmreclem4  16939  prmreclem5  16940  hashbccl  17023  prmgaplem3  17073  prmgaplem4  17074  prdsds  17480  mrcflem  17620  isacs1i  17671  wunnat  17975  dmcoass  18082  lublecl  18375  lubid  18376  rabsubmgmd  18686  mgmhmeql  18698  issubmd  18788  mhmeql  18808  cntzval  19308  cntzssv  19315  symgsssg  19453  symgfisg  19454  pmtrdifellem4  19465  odfval  19518  odlem1  19521  odlem2  19525  odngen  19563  gexlem1  19565  gexlem2  19568  sylow2alem2  19604  sylow2blem3  19608  oddvdssubg  19841  cyggex2  19883  ablfaclem3  20075  rgspncl  20581  lssacs  20933  lspf  20940  ocvfval  21638  ocvval  21639  dsmmval2  21710  dsmmsubg  21717  asplss  21848  aspsubrg  21850  psrass1lem  21906  psrdi  21939  psrdir  21940  psrass23l  21941  psrass23  21943  resspsrmul  21950  mplbas  21964  mplsubglem  21973  mplsubrglem  21978  mplmonmul  22008  psropprmul  22187  scmatlss  22479  smadiadet  22624  pmatcoe1fsupp  22655  cpmatsubgpmat  22674  fctop  22958  cctop  22960  ppttop  22961  epttop  22963  clscld  23001  neips  23067  neiptopnei  23086  ordtbaslem  23142  ordtuni  23144  ordtcld1  23151  ordtcld2  23152  cnpfval  23188  iscnp2  23193  cmpcov2  23344  cmpsublem  23353  tgcmp  23355  conncompcld  23388  1stcfb  23399  2ndc1stc  23405  2ndcdisj  23410  finlocfin  23474  kgentopon  23492  xkotf  23539  txkgen  23606  xkococnlem  23613  imastopn  23674  kqffn  23679  opnfbas  23796  flimfnfcls  23982  alexsubALT  24005  ptcmplem2  24007  symgtgp  24060  tgpconncompeqg  24066  tgpconncomp  24067  ghmcnp  24069  tsmsfbas  24082  eltsms  24087  utoptop  24189  utopbas  24190  blfvalps  24338  blfps  24361  blf  24362  nmoffn  24668  nmofval  24671  nmogelb  24673  nmolb  24674  nmof  24676  ishtpy  24940  clsocv  25220  rrxnm  25361  rrxbasefi  25380  minveclem3b  25398  minveclem4  25402  ovolcl  25449  ovollb  25450  ovolgelb  25451  ovolge0  25452  ovolshftlem1  25480  ovolshft  25482  ovolscalem1  25484  ovolscalem2  25485  ovolsca  25486  ovolicc2lem3  25490  shftmbl  25509  iundisj  25519  dyadmax  25569  dyadmbllem  25570  opnmbllem  25572  mdegmullem  26053  uc1pval  26115  mon1pval  26117  elqaalem1  26297  elqaalem3  26299  aannenlem2  26307  aalioulem2  26311  radcnvcl  26396  radcnvlt1  26397  radcnvle  26399  ftalem4  27055  ftalem5  27056  efnnfsumcl  27082  isppw  27093  sgmval2  27122  efchtdvds  27138  sqff1o  27161  fsumdvdsdiaglem  27162  fsumdvdsdiag  27163  fsumdvdscom  27164  musum  27170  muinv  27172  sgmmul  27181  ppiub  27184  vmasum  27196  logfac2  27197  perfectlem2  27210  lgsfcl  27285  lgscl  27291  lgsquadlem1  27360  lgsquadlem2  27361  rpvmasumlem  27467  mudivsum  27510  mulogsum  27512  mulog2sumlem2  27515  vmalogdivsum2  27518  logsqvma  27522  logsqvma2  27523  selberglem3  27527  selberg  27528  selberg34r  27551  pntsval2  27556  pntrlog2bndlem1  27557  sltval2  27637  conway  27780  eqscut2  27787  scutun12  27791  scutbdaybnd  27796  scutbdaybnd2  27797  scutbdaylt  27799  bday1s  27812  cuteq0  27813  madef  27831  leftssold  27853  rightssold  27854  madebdaylemlrcut  27873  cofcut1  27890  cofcutr  27894  cutlt  27902  precsexlem8  28174  precsexlem11  28177  onssno  28213  tglnunirn  28492  tglnssp  28496  incistruhgr  29024  upgrss  29033  upgrn0  29034  upgruhgr  29047  usgrss  29119  uspgrushgr  29122  ushgredgedg  29174  ushgredgedgloop  29176  vtxdun  29427  vtxdginducedm1  29489  wlknwwlksnbij  29836  hashwwlksnext  29862  frcond3  30216  numclwlk1lem2  30317  ocsh  31230  spancl  31283  shsval2i  31334  ococin  31355  chsupid  31359  speccl  31846  hatomistici  32309  chpssati  32310  iundisjf  32537  aciunf1  32608  fpwrelmap  32679  iundisjfi  32737  pwrssmgc  32929  cycpmco2f1  33083  cycpmco2rn  33084  cycpmco2lem1  33085  cycpmco2lem2  33086  cycpmco2lem3  33087  cycpmco2lem4  33088  cycpmco2lem5  33089  cycpmco2lem6  33090  cycpmco2lem7  33091  cycpmco2  33092  nsgmgclem  33374  constrsuc  33718  locfinreflem  33798  zarclsiin  33829  zarcls  33832  zartopn  33833  esumrnmpt2  34028  esumpinfval  34033  sigagensiga  34101  ldgenpisyslem1  34123  ldgenpisys  34126  measvuni  34174  imambfm  34223  dya2iocuni  34244  omscl  34256  oms0  34258  omsmon  34259  omssubadd  34261  carsgcl  34265  oddpwdc  34315  eulerpartlem1  34328  eulerpartlemt  34332  eulerpartgbij  34333  eulerpartlemmf  34336  eulerpartlemgh  34339  eulerpartlemgs2  34341  ballotlem2  34450  ballotlemfc0  34454  ballotlemfcc  34455  ballotlemfmpn  34456  ballotlemiex  34463  ballotlemsup  34466  ballotlem7  34497  ballotth  34499  reprpmtf1o  34600  breprexplema  34604  hgt750lema  34631  bnj110  34831  bnj1204  34985  bnj1311  34997  fnrelpredd  35062  subfacp1lem6  35149  erdszelem2  35156  connpconn  35199  cvmliftmolem2  35246  cvmliftlem15  35262  cvmlift2lem12  35278  snmlff  35293  satfrnmapom  35334  rankeq1o  36131  finminlem  36278  fnessref  36317  neibastop1  36319  neibastop2lem  36320  weiunlem2  36423  weiunse  36428  bj-rabtr  36890  bj-rabtrAUTO  36892  bj-vecssmod  37241  icoreresf  37312  phpreu  37570  fin2so  37573  poimirlem26  37612  poimirlem31  37617  poimirlem32  37618  opnmbllem0  37622  mblfinlem1  37623  mblfinlem2  37624  ismblfin  37627  mbfposadd  37633  cnambfre  37634  cover2  37681  indexa  37699  fdc  37711  sstotbnd2  37740  sstotbnd3  37742  igenidl  38029  prnc  38033  toycom  38933  lkrlss  39055  atlatmstc  39279  atlatle  39280  glbconN  39337  glbconNOLD  39338  linepsubN  39713  pmapssat  39720  pmaple  39722  pmapsub  39729  paddssat  39775  diass  41003  diaglbN  41016  diaintclN  41019  diassdvaN  41021  docaclN  41085  dibglbN  41127  dibintclN  41128  diclspsn  41155  dihglblem2N  41255  dih1dimatlem  41290  dihglb2  41303  dochval2  41313  dochcl  41314  dochvalr  41318  doch2val2  41325  dochss  41326  dochocss  41327  lclkr  41494  lclkrs  41500  lcdvbase  41554  lcdvbasess  41555  mapdunirnN  41611  aks4d1p4  42039  aks4d1p5  42040  aks4d1p7  42043  aks4d1p8  42047  sticksstones1  42106  aks6d1c6lem2  42131  grpods  42154  unitscyglem1  42155  unitscyglem2  42156  unitscyglem4  42158  mhpind  42567  mhphf  42570  prjcrv0  42606  infdesc  42616  mzpindd  42720  fiphp3d  42793  rencldnfilem  42794  irrapx1  42802  pellexlem3  42805  pellfundre  42855  pellfundge  42856  pellfundlb  42858  pellfundglb  42859  jm2.22  42970  jm2.23  42971  rpnnen3  43007  pwssplit4  43064  pwfi2f1o  43071  hbtlem6  43104  dgraalem  43120  dgraaub  43123  itgocn  43139  onintunirab  43202  nadd2rabord  43360  nadd1rabord  43364  rfovcnvf1od  43979  fsovfd  43987  fsovcnvlem  43988  binomcxplemdvbinom  44329  binomcxplemcvg  44330  binomcxplemnotnn0  44332  uzwo4  45015  disjf1o  45153  icof  45181  allbutfiinf  45388  supminfxr  45432  supminfxr2  45437  fsumsupp0  45550  sumnnodd  45602  fnlimabslt  45651  liminfvalxr  45755  ioodvbdlimc1lem1  45903  dvnprodlem1  45918  dvnprodlem2  45919  stoweidlem14  45986  stoweidlem34  46006  stoweidlem44  46016  stoweidlem50  46022  stoweidlem51  46023  stoweidlem52  46024  stoweidlem57  46029  stoweidlem59  46031  fourierdlem19  46098  fourierdlem20  46099  fourierdlem25  46104  fourierdlem31  46110  fourierdlem37  46116  fourierdlem42  46121  fourierdlem51  46129  fourierdlem54  46132  fourierdlem64  46142  fourierdlem79  46157  elaa2lem  46205  etransclem16  46222  etransclem24  46230  etransclem31  46237  etransclem33  46239  etransclem34  46240  etransclem48  46254  salgencl  46304  salexct  46306  salgenuni  46309  subsaliuncllem  46329  meadjiunlem  46437  caragenss  46476  caratheodory  46500  ovnlecvr  46530  ovnlerp  46534  ovn0lem  46537  ovnsubaddlem1  46542  hoidmv1lelem1  46563  hoidmv1lelem3  46565  hoidmvlelem1  46567  hoidmvlelem2  46568  hoidmvlelem3  46569  hoidmvlelem4  46570  ovnhoilem1  46573  ovnhoilem2  46574  ovnlecvr2  46582  ovncvr2  46583  opnvonmbllem2  46605  ovolval4lem1  46621  pimconstlt1  46674  pimiooltgt  46682  pimgtmnf2  46686  pimdecfgtioc  46687  pimincfltioc  46688  pimdecfgtioo  46689  pimincfltioo  46690  sssmf  46710  incsmflem  46713  smfaddlem1  46735  smfaddlem2  46736  decsmflem  46738  smflimlem1  46743  smflimlem2  46744  smflimlem3  46745  smfrec  46761  smfmullem4  46766  smfdiv  46769  smfsuplem1  46783  smfsuplem3  46785  smfinflem  46789  smflimsuplem1  46792  smflimsuplem7  46798  smfliminflem  46802  sprsymrelfolem1  47437  prmdvdsfmtnof1lem1  47529  prmdvdsfmtnof  47531  perfectALTVlem2  47667  isubgredg  47810  isubgruhgr  47812  isubgrgrim  47855  uhgrimisgrgric  47857  uspgrlimlem1  47913  uspgrlimlem4  47916  uspgrlim  47917  grlimgrtrilem2  47920  oddibas  48047  2zlidl  48114  2zrngbas  48116  2zrng0  48118  isclatd  48840  topclat  48855