Theorem ssrab2 4028

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

This proof depends on syntax axioms:  {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:  ssrab3  4030  ssrabeq  4032  iinrab2  5028  riinrab  5044  rabelpw  5298  frminex  5630  wereu2  5648  predres  6341  frpomin  6342  frpoinsg  6345  ssimaex  6968  f1oresrab  7126  weniso  7362  canth  7372  riotacl  7392  riotassuni  7415  onminesb  7805  onminsb  7806  onintrab  7808  onnminsb  7811  onminex  7814  tfisg  7863  tfis  7864  suppssdm  8187  fnsuppres  8201  oeeulem  8603  nnawordex  8639  pmvalg  8850  fineqvlem  9250  ordtypelem3  9507  ordtypelem4  9508  ordtypelem6  9510  hartogs  9531  card2on  9541  wdom2d  9567  oemapvali  9678  frinsg  9748  tz9.12lem1  9787  tz9.12lem3  9789  rankf  9795  cardf2  10017  cardid2  10027  cardmin2  10073  acni3  10119  dfac2a  10201  cofsmo  10340  coftr  10344  fin2i2  10389  isfin2-2  10390  enfin2i  10392  fin1a2lem11  10481  fin1a2lem12  10482  axdc3lem4  10524  ac6  10551  ondomon  10640  alephval2  10650  pwfseqlem1  10736  pwfseqlem3  10738  wunccl  10822  tskmcl  10919  infm3  12269  uzf  12961  nnwos  13035  supminf  13055  zsupss  13057  rpnnen1lem1  13099  rpnnen1lem3  13100  rpnnen1lem5  13102  ixxf  13479  fzf  13636  flval3  13948  rabssnn0fi  14122  expge0  14234  expge1  14235  hashbclem  14590  01sqrexlem3  15404  rlimrege0  15739  incexc2  16000  bitsf  16590  bitsfzolem  16597  sadadd2lem  16622  sadadd3  16624  sadcl  16625  smupf  16641  smuval2  16645  smupvallem  16646  smucl  16647  smueqlem  16653  lcmcllem  16764  lcmn0cl  16765  lcmledvds  16767  lcmfval  16789  lcmfcllem  16793  lcmfn0cl  16794  lcmfledvds  16800  phicl2  16938  phibnd  16941  hashdvds  16945  phiprmpw  16946  phimullem  16949  eulerth  16953  phisum  16961  odzcllem  16963  odzdvds  16966  prmreclem1  17087  prmreclem2  17088  prmreclem3  17089  prmreclem4  17090  prmreclem5  17091  hashbccl  17174  prmgaplem3  17224  prmgaplem4  17225  prdsds  17628  mrcflem  17773  isacs1i  17824  wunnat  18127  dmcoass  18234  lublecl  18526  lubid  18527  rabsubmgmd  18886  mgmhmeql  18898  issubmd  18994  mhmeql  19015  cntzval  19528  cntzssv  19535  symgsssg  19674  symgfisg  19675  pmtrdifellem4  19686  odfval  19739  odlem1  19742  odlem2  19746  odngen  19784  gexlem1  19786  gexlem2  19789  sylow2alem2  19825  sylow2blem3  19829  oddvdssubg  20062  cyggex2  20104  ablfaclem3  20296  rgspncl  20858  lssacs  21235  lspf  21242  ocvfval  21965  ocvval  21966  dsmmval2  22035  dsmmsubg  22042  asplss  22174  aspsubrg  22176  psrass1lem  22234  psrdi  22265  psrdir  22266  psrass23l  22267  psrass23  22269  resspsrmul  22276  mplbas  22290  mplsubglem  22299  mplsubrglem  22304  mplmonmul  22338  psropprmul  22548  scmatlss  22833  smadiadet  22978  pmatcoe1fsupp  23012  cpmatsubgpmat  23031  fctop  23315  cctop  23317  ppttop  23318  epttop  23320  clscld  23358  neips  23424  neiptopnei  23443  ordtbaslem  23499  ordtuni  23501  ordtcld1  23508  ordtcld2  23509  cnpfval  23545  iscnp2  23550  cmpcov2  23701  cmpsublem  23710  tgcmp  23712  conncompcld  23745  1stcfb  23756  2ndc1stc  23762  2ndcdisj  23768  finlocfin  23832  kgentopon  23850  xkotf  23897  txkgen  23964  xkococnlem  23971  imastopn  24032  kqffn  24037  opnfbas  24154  flimfnfcls  24340  alexsubALT  24363  ptcmplem2  24365  symgtgp  24418  tgpconncompeqg  24424  tgpconncomp  24425  ghmcnp  24427  tsmsfbas  24440  eltsms  24445  utoptop  24546  utopbas  24547  blfvalps  24695  blfps  24718  blf  24719  nmoffn  25023  nmofval  25026  nmogelb  25028  nmolb  25029  nmof  25031  ishtpy  25286  clsocv  25564  rrxnm  25705  rrxbasefi  25724  minveclem3b  25742  minveclem4  25746  ovolcl  25792  ovollb  25793  ovolgelb  25794  ovolge0  25795  ovolshftlem1  25823  ovolshft  25825  ovolscalem1  25827  ovolscalem2  25828  ovolsca  25829  ovolicc2lem3  25833  shftmbl  25852  iundisj  25862  dyadmax  25912  dyadmbllem  25913  opnmbllem  25915  mdegmullem  26389  uc1pval  26451  mon1pval  26453  elqaalem1  26635  elqaalem3  26637  aannenlem2  26649  aalioulem2  26653  radcnvcl  26737  radcnvlt1  26738  radcnvle  26740  ftalem4  27396  ftalem5  27397  efnnfsumcl  27423  isppw  27434  sgmval2  27463  efchtdvds  27479  sqff1o  27502  fsumdvdsdiaglem  27503  fsumdvdsdiag  27504  fsumdvdscom  27505  musum  27511  muinv  27513  sgmmul  27521  ppiub  27524  vmasum  27536  logfac2  27537  perfectlem2  27550  lgsfcl  27625  lgscl  27631  lgsquadlem1  27700  lgsquadlem2  27701  rpvmasumlem  27807  mudivsum  27850  mulogsum  27852  mulog2sumlem2  27855  vmalogdivsum2  27858  logsqvma  27862  logsqvma2  27863  selberglem3  27867  selberg  27868  selberg34r  27891  pntsval2  27896  pntrlog2bndlem1  27897  infdesc  27960  ltsval2  28006  conway  28158  eqcuts2  28165  cutsun12  28169  cutbdaybnd  28174  cutbdaybnd2  28175  cutbdaylt  28177  bday1  28193  cuteq0  28194  madef  28215  leftssold  28250  rightssold  28251  madebdaylemlrcut  28278  sltsbday  28296  cofcut1  28299  cofcutr  28303  cutlt  28311  precsexlem8  28593  precsexlem11  28596  onssno  28633  oncutlt  28643  oniso  28650  bdayons  28655  bdayn0p1  28748  tglnunirn  29004  tglnssp  29008  plngrnssp  29250  plngssp  29252  incistruhgr  29650  upgrss  29659  upgrn0  29660  upgruhgr  29673  usgrss  29748  uspgrushgr  29751  ushgredgedg  29803  ushgredgedgloop  29805  vtxdun  30055  vtxdginducedm1  30117  wlknwwlksnbij  30470  hashwwlksnext  30496  frcond3  30863  numclwlk1lem2  30964  ocsh  31878  spancl  31931  shsval2i  31982  ococin  32003  chsupid  32007  speccl  32494  hatomistici  32957  chpssati  32958  iundisjf  33176  aciunf1  33250  fpwrelmap  33318  iundisjfi  33381  pwrssmgc  33554  cycpmco2f1  33678  cycpmco2rn  33679  cycpmco2lem1  33680  cycpmco2lem2  33681  cycpmco2lem3  33682  cycpmco2lem4  33683  cycpmco2lem5  33684  cycpmco2lem6  33685  cycpmco2lem7  33686  cycpmco2  33687  fxpss  33720  nsgmgclem  33955  0mplrim  34139  selvply1rhmlemb  34144  selvply1rhm0  34151  extvfvcl  34161  mplmulmvr  34164  evlextv  34167  mplvrpmlem  34168  mplvrpmga  34170  mplvrpmrhm  34172  psrmonmul  34175  esplylem  34191  esplympl  34192  esplymhp  34193  esplyfv1  34194  esplyfv  34195  esplyfval3  34197  esplyfval1  34198  esplyfvaln  34199  constrsuc  34363  locfinreflem  34465  zarclsiin  34496  zarcls  34499  zartopn  34500  esumrnmpt2  34693  esumpinfval  34698  sigagensiga  34767  ldgenpisyslem1  34789  ldgenpisys  34792  measvuni  34840  imambfm  34887  dya2iocuni  34908  omscl  34920  oms0  34922  omsmon  34923  omssubadd  34925  carsgcl  34929  oddpwdc  34979  eulerpartlem1  34992  eulerpartlemt  34996  eulerpartgbij  34997  eulerpartlemmf  35000  eulerpartlemgh  35003  eulerpartlemgs2  35005  ballotlem2  35114  ballotlemfc0  35118  ballotlemfcc  35119  ballotlemfmpn  35120  ballotlemiex  35127  ballotlemsup  35130  ballotlem7  35161  ballotth  35163  reprpmtf1o  35248  breprexplema  35252  hgt750lema  35279  bnj110  35481  bnj1204  35635  bnj1311  35647  fnrelpredd  35709  subfacp1lem6  35929  erdszelem2  35936  connpconn  35979  cvmliftmolem2  36026  cvmliftlem15  36042  cvmlift2lem12  36058  snmlff  36073  satfrnmapom  36114  rankeq1o  36912  nmuladdel  36941  finminlem  37086  fnessref  37125  neibastop1  37127  neibastop2lem  37128  weiunlem  37231  weiunse  37236  bj-rabtr  37823  bj-rabtrAUTO  37825  bj-vecssmod  38182  icoreresf  38255  phpreu  38507  fin2so  38510  poimirlem26  38544  poimirlem31  38549  poimirlem32  38550  opnmbllem0  38554  mblfinlem1  38555  mblfinlem2  38556  ismblfin  38559  mbfposadd  38565  cnambfre  38566  cover2  38629  indexa  38647  fdc  38659  sstotbnd2  38688  sstotbnd3  38690  igenidl  38977  prnc  38981  toycom  40010  lkrlss  40132  atlatmstc  40356  atlatle  40357  glbconN  40414  linepsubN  40789  pmapssat  40796  pmaple  40798  pmapsub  40805  paddssat  40851  diass  42079  diaglbN  42092  diaintclN  42095  diassdvaN  42097  docaclN  42161  dibglbN  42203  dibintclN  42204  diclspsn  42231  dihglblem2N  42331  dih1dimatlem  42366  dihglb2  42379  dochval2  42389  dochcl  42390  dochvalr  42394  doch2val2  42401  dochss  42402  dochocss  42403  lclkr  42570  lclkrs  42576  lcdvbase  42630  lcdvbasess  42631  mapdunirnN  42687  aks4d1p4  43109  aks4d1p5  43110  aks4d1p7  43113  aks4d1p8  43117  sticksstones1  43176  aks6d1c6lem2  43201  grpods  43224  unitscyglem1  43225  unitscyglem2  43226  unitscyglem4  43228  mhpind  43602  mhphf  43605  frlmnzcoordinf  43634  frlmnzcoordcl  43635  frlmnzcoordn0  43637  prjcrv0  43649  mzpindd  43736  fiphp3d  43805  rencldnfilem  43806  irrapx1  43814  pellexlem3  43817  pellfundre  43867  pellfundge  43868  pellfundlb  43870  pellfundglb  43871  jm2.22  43981  jm2.23  43982  rpnnen3  44018  pwssplit4  44075  pwfi2f1o  44082  hbtlem6  44115  dgraalem  44131  dgraaub  44134  itgocn  44150  onintunirab  44213  nadd2rabord  44371  nadd1rabord  44375  rfovcnvf1od  44989  fsovfd  44997  fsovcnvlem  44998  binomcxplemdvbinom  45322  binomcxplemcvg  45323  binomcxplemnotnn0  45325  uzwo4  46039  disjf1o  46175  icof  46201  allbutfiinf  46399  supminfxr  46443  supminfxr2  46448  fsumsupp0  46559  sumnnodd  46611  fnlimabslt  46658  liminfvalxr  46762  ioodvbdlimc1lem1  46910  dvnprodlem1  46925  dvnprodlem2  46926  stoweidlem14  46993  stoweidlem34  47013  stoweidlem44  47023  stoweidlem50  47029  stoweidlem51  47030  stoweidlem52  47031  stoweidlem57  47036  stoweidlem59  47038  fourierdlem19  47105  fourierdlem20  47106  fourierdlem25  47111  fourierdlem31  47117  fourierdlem37  47123  fourierdlem42  47128  fourierdlem51  47136  fourierdlem54  47139  fourierdlem64  47149  fourierdlem79  47164  elaa2lem  47212  etransclem16  47229  etransclem24  47237  etransclem31  47244  etransclem33  47246  etransclem34  47247  etransclem48  47261  salgencl  47311  salexct  47313  salgenuni  47316  subsaliuncllem  47336  meadjiunlem  47444  caragenss  47483  caratheodory  47507  ovnlecvr  47537  ovnlerp  47541  ovn0lem  47544  ovnsubaddlem1  47549  hoidmv1lelem1  47570  hoidmv1lelem3  47572  hoidmvlelem1  47574  hoidmvlelem2  47575  hoidmvlelem3  47576  hoidmvlelem4  47577  ovnhoilem1  47580  ovnhoilem2  47581  ovnlecvr2  47589  ovncvr2  47590  opnvonmbllem2  47612  ovolval4lem1  47628  pimconstlt1  47681  pimgtmnf2  47693  pimdecfgtioc  47694  pimincfltioc  47695  pimdecfgtioo  47696  pimincfltioo  47697  sssmf  47717  incsmflem  47720  smfaddlem1  47742  smfaddlem2  47743  decsmflem  47745  smflimlem1  47750  smflimlem2  47751  smflimlem3  47752  smfrec  47768  smfmullem4  47773  smfdiv  47776  smfpimcclem  47786  smfsuplem1  47790  smfsuplem3  47792  smfinflem  47796  smflimsuplem1  47799  smflimsuplem7  47805  smfliminflem  47809  tmachlem-agreeself  47915  tmachlem-agreeprod  47916  tmachlem-uassst  47922  tmachlem-extpcover  47924  tmachlem-agreefin  47927  sprsymrelfolem1  48543  prmdvdsfmtnof1lem1  48638  prmdvdsfmtnof  48640  perfectALTVlem2  48789  isubgredg  48933  isubgruhgr  48935  isubgrgrim  48996  uhgrimisgrgric  48998  uspgrlimlem1  49055  uspgrlimlem4  49058  uspgrlim  49059  grlimgrtrilem2  49069  oddibas  49239  2zlidl  49306  2zrngbas  49308  2zrng0  49310  isclatd  50060  topclat  50075  dvsec  50825  dvcsc  50826  dvcot  50827