Theorem ssrab2 4034

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

Syntax hints:  {crab 3401   ⊆ wss 3903

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 3402  df-ss 3920

This theorem is referenced by:  ssrab3  4036  ssrabeq  4038  iinrab2  5027  riinrab  5041  rabelpw  5283  rabexgOLD  5285  frminex  5611  wereu2  5629  predres  6305  frpomin  6306  frpoinsg  6309  ssimaex  6927  f1oresrab  7082  weniso  7310  canth  7322  riotacl  7342  riotassuni  7365  onminesb  7748  onminsb  7749  onintrab  7751  onnminsb  7754  onminex  7757  tfisg  7806  tfis  7807  suppssdm  8129  fnsuppres  8143  oeeulem  8539  nnawordex  8575  pmvalg  8786  fineqvlem  9178  ordtypelem3  9437  ordtypelem4  9438  ordtypelem6  9440  hartogs  9461  card2on  9471  wdom2d  9497  oemapvali  9605  frinsg  9675  tz9.12lem1  9711  tz9.12lem3  9713  rankf  9718  cardf2  9867  cardid2  9877  cardmin2  9923  acni3  9969  dfac2a  10052  cofsmo  10191  coftr  10195  fin2i2  10240  isfin2-2  10241  enfin2i  10243  fin1a2lem11  10332  fin1a2lem12  10333  axdc3lem4  10375  ac6  10402  ondomon  10485  alephval2  10495  pwfseqlem1  10581  pwfseqlem3  10583  wunccl  10667  tskmcl  10764  infm3  12113  uzf  12766  nnwos  12840  supminf  12860  zsupss  12862  rpnnen1lem1  12903  rpnnen1lem3  12904  rpnnen1lem5  12906  ixxf  13283  fzf  13439  flval3  13747  rabssnn0fi  13921  expge0  14033  expge1  14034  hashbclem  14387  01sqrexlem3  15179  rlimrege0  15514  incexc2  15773  bitsf  16366  bitsfzolem  16373  sadadd2lem  16398  sadadd3  16400  sadcl  16401  smupf  16417  smuval2  16421  smupvallem  16422  smucl  16423  smueqlem  16429  lcmcllem  16535  lcmn0cl  16536  lcmledvds  16538  lcmfval  16560  lcmfcllem  16564  lcmfn0cl  16565  lcmfledvds  16571  phicl2  16707  phibnd  16710  hashdvds  16714  phiprmpw  16715  phimullem  16718  eulerth  16722  phisum  16730  odzcllem  16732  odzdvds  16735  prmreclem1  16856  prmreclem2  16857  prmreclem3  16858  prmreclem4  16859  prmreclem5  16860  hashbccl  16943  prmgaplem3  16993  prmgaplem4  16994  prdsds  17396  mrcflem  17541  isacs1i  17592  wunnat  17895  dmcoass  18002  lublecl  18294  lubid  18295  rabsubmgmd  18641  mgmhmeql  18653  issubmd  18743  mhmeql  18763  cntzval  19262  cntzssv  19269  symgsssg  19408  symgfisg  19409  pmtrdifellem4  19420  odfval  19473  odlem1  19476  odlem2  19480  odngen  19518  gexlem1  19520  gexlem2  19523  sylow2alem2  19559  sylow2blem3  19563  oddvdssubg  19796  cyggex2  19838  ablfaclem3  20030  rgspncl  20558  lssacs  20930  lspf  20937  ocvfval  21633  ocvval  21634  dsmmval2  21703  dsmmsubg  21710  asplss  21841  aspsubrg  21843  psrass1lem  21900  psrdi  21932  psrdir  21933  psrass23l  21934  psrass23  21936  resspsrmul  21943  mplbas  21957  mplsubglem  21966  mplsubrglem  21971  mplmonmul  22003  psropprmul  22190  scmatlss  22481  smadiadet  22626  pmatcoe1fsupp  22657  cpmatsubgpmat  22676  fctop  22960  cctop  22962  ppttop  22963  epttop  22965  clscld  23003  neips  23069  neiptopnei  23088  ordtbaslem  23144  ordtuni  23146  ordtcld1  23153  ordtcld2  23154  cnpfval  23190  iscnp2  23195  cmpcov2  23346  cmpsublem  23355  tgcmp  23357  conncompcld  23390  1stcfb  23401  2ndc1stc  23407  2ndcdisj  23412  finlocfin  23476  kgentopon  23494  xkotf  23541  txkgen  23608  xkococnlem  23615  imastopn  23676  kqffn  23681  opnfbas  23798  flimfnfcls  23984  alexsubALT  24007  ptcmplem2  24009  symgtgp  24062  tgpconncompeqg  24068  tgpconncomp  24069  ghmcnp  24071  tsmsfbas  24084  eltsms  24089  utoptop  24190  utopbas  24191  blfvalps  24339  blfps  24362  blf  24363  nmoffn  24667  nmofval  24670  nmogelb  24672  nmolb  24673  nmof  24675  ishtpy  24939  clsocv  25218  rrxnm  25359  rrxbasefi  25378  minveclem3b  25396  minveclem4  25400  ovolcl  25447  ovollb  25448  ovolgelb  25449  ovolge0  25450  ovolshftlem1  25478  ovolshft  25480  ovolscalem1  25482  ovolscalem2  25483  ovolsca  25484  ovolicc2lem3  25488  shftmbl  25507  iundisj  25517  dyadmax  25567  dyadmbllem  25568  opnmbllem  25570  mdegmullem  26051  uc1pval  26113  mon1pval  26115  elqaalem1  26295  elqaalem3  26297  aannenlem2  26305  aalioulem2  26309  radcnvcl  26394  radcnvlt1  26395  radcnvle  26397  ftalem4  27054  ftalem5  27055  efnnfsumcl  27081  isppw  27092  sgmval2  27121  efchtdvds  27137  sqff1o  27160  fsumdvdsdiaglem  27161  fsumdvdsdiag  27162  fsumdvdscom  27163  musum  27169  muinv  27171  sgmmul  27180  ppiub  27183  vmasum  27195  logfac2  27196  perfectlem2  27209  lgsfcl  27284  lgscl  27290  lgsquadlem1  27359  lgsquadlem2  27360  rpvmasumlem  27466  mudivsum  27509  mulogsum  27511  mulog2sumlem2  27514  vmalogdivsum2  27517  logsqvma  27521  logsqvma2  27522  selberglem3  27526  selberg  27527  selberg34r  27550  pntsval2  27555  pntrlog2bndlem1  27556  ltsval2  27636  conway  27787  eqcuts2  27794  cutsun12  27798  cutbdaybnd  27803  cutbdaybnd2  27804  cutbdaylt  27806  bday1  27822  cuteq0  27823  madef  27844  leftssold  27879  rightssold  27880  madebdaylemlrcut  27907  sltsbday  27925  cofcut1  27928  cofcutr  27932  cutlt  27940  precsexlem8  28222  precsexlem11  28225  onssno  28262  oncutlt  28272  oniso  28279  bdayons  28284  bdayn0p1  28377  tglnunirn  28632  tglnssp  28636  incistruhgr  29164  upgrss  29173  upgrn0  29174  upgruhgr  29187  usgrss  29259  uspgrushgr  29262  ushgredgedg  29314  ushgredgedgloop  29316  vtxdun  29567  vtxdginducedm1  29629  wlknwwlksnbij  29973  hashwwlksnext  29999  frcond3  30356  numclwlk1lem2  30457  ocsh  31370  spancl  31423  shsval2i  31474  ococin  31495  chsupid  31499  speccl  31986  hatomistici  32449  chpssati  32450  iundisjf  32675  aciunf1  32752  fpwrelmap  32822  iundisjfi  32886  pwrssmgc  33092  cycpmco2f1  33217  cycpmco2rn  33218  cycpmco2lem1  33219  cycpmco2lem2  33220  cycpmco2lem3  33221  cycpmco2lem4  33222  cycpmco2lem5  33223  cycpmco2lem6  33224  cycpmco2lem7  33225  cycpmco2  33226  fxpss  33259  nsgmgclem  33503  extvfvcl  33712  mplmulmvr  33715  evlextv  33718  mplvrpmlem  33719  mplvrpmga  33721  mplvrpmrhm  33723  psrmonmul  33726  esplylem  33742  esplympl  33743  esplymhp  33744  esplyfv1  33745  esplyfv  33746  esplyfval3  33748  esplyfval1  33749  esplyfvaln  33750  constrsuc  33915  locfinreflem  34017  zarclsiin  34048  zarcls  34051  zartopn  34052  esumrnmpt2  34245  esumpinfval  34250  sigagensiga  34318  ldgenpisyslem1  34340  ldgenpisys  34343  measvuni  34391  imambfm  34439  dya2iocuni  34460  omscl  34472  oms0  34474  omsmon  34475  omssubadd  34477  carsgcl  34481  oddpwdc  34531  eulerpartlem1  34544  eulerpartlemt  34548  eulerpartgbij  34549  eulerpartlemmf  34552  eulerpartlemgh  34555  eulerpartlemgs2  34557  ballotlem2  34666  ballotlemfc0  34670  ballotlemfcc  34671  ballotlemfmpn  34672  ballotlemiex  34679  ballotlemsup  34682  ballotlem7  34713  ballotth  34715  reprpmtf1o  34803  breprexplema  34807  hgt750lema  34834  bnj110  35033  bnj1204  35187  bnj1311  35199  fnrelpredd  35266  subfacp1lem6  35398  erdszelem2  35405  connpconn  35448  cvmliftmolem2  35495  cvmliftlem15  35511  cvmlift2lem12  35527  snmlff  35542  satfrnmapom  35583  rankeq1o  36384  finminlem  36531  fnessref  36570  neibastop1  36572  neibastop2lem  36573  weiunlem  36676  weiunse  36681  bj-rabtr  37172  bj-rabtrAUTO  37174  bj-vecssmod  37530  icoreresf  37601  phpreu  37849  fin2so  37852  poimirlem26  37891  poimirlem31  37896  poimirlem32  37897  opnmbllem0  37901  mblfinlem1  37902  mblfinlem2  37903  ismblfin  37906  mbfposadd  37912  cnambfre  37913  cover2  37960  indexa  37978  fdc  37990  sstotbnd2  38019  sstotbnd3  38021  igenidl  38308  prnc  38312  toycom  39343  lkrlss  39465  atlatmstc  39689  atlatle  39690  glbconN  39747  linepsubN  40122  pmapssat  40129  pmaple  40131  pmapsub  40138  paddssat  40184  diass  41412  diaglbN  41425  diaintclN  41428  diassdvaN  41430  docaclN  41494  dibglbN  41536  dibintclN  41537  diclspsn  41564  dihglblem2N  41664  dih1dimatlem  41699  dihglb2  41712  dochval2  41722  dochcl  41723  dochvalr  41727  doch2val2  41734  dochss  41735  dochocss  41736  lclkr  41903  lclkrs  41909  lcdvbase  41963  lcdvbasess  41964  mapdunirnN  42020  aks4d1p4  42443  aks4d1p5  42444  aks4d1p7  42447  aks4d1p8  42451  sticksstones1  42510  aks6d1c6lem2  42535  grpods  42558  unitscyglem1  42559  unitscyglem2  42560  unitscyglem4  42562  mhpind  42946  mhphf  42949  prjcrv0  42985  infdesc  42995  mzpindd  43097  fiphp3d  43170  rencldnfilem  43171  irrapx1  43179  pellexlem3  43182  pellfundre  43232  pellfundge  43233  pellfundlb  43235  pellfundglb  43236  jm2.22  43346  jm2.23  43347  rpnnen3  43383  pwssplit4  43440  pwfi2f1o  43447  hbtlem6  43480  dgraalem  43496  dgraaub  43499  itgocn  43515  onintunirab  43578  nadd2rabord  43736  nadd1rabord  43740  rfovcnvf1od  44354  fsovfd  44362  fsovcnvlem  44363  binomcxplemdvbinom  44703  binomcxplemcvg  44704  binomcxplemnotnn0  44706  uzwo4  45407  disjf1o  45544  icof  45571  allbutfiinf  45772  supminfxr  45816  supminfxr2  45821  fsumsupp0  45932  sumnnodd  45984  fnlimabslt  46031  liminfvalxr  46135  ioodvbdlimc1lem1  46283  dvnprodlem1  46298  dvnprodlem2  46299  stoweidlem14  46366  stoweidlem34  46386  stoweidlem44  46396  stoweidlem50  46402  stoweidlem51  46403  stoweidlem52  46404  stoweidlem57  46409  stoweidlem59  46411  fourierdlem19  46478  fourierdlem20  46479  fourierdlem25  46484  fourierdlem31  46490  fourierdlem37  46496  fourierdlem42  46501  fourierdlem51  46509  fourierdlem54  46512  fourierdlem64  46522  fourierdlem79  46537  elaa2lem  46585  etransclem16  46602  etransclem24  46610  etransclem31  46617  etransclem33  46619  etransclem34  46620  etransclem48  46634  salgencl  46684  salexct  46686  salgenuni  46689  subsaliuncllem  46709  meadjiunlem  46817  caragenss  46856  caratheodory  46880  ovnlecvr  46910  ovnlerp  46914  ovn0lem  46917  ovnsubaddlem1  46922  hoidmv1lelem1  46943  hoidmv1lelem3  46945  hoidmvlelem1  46947  hoidmvlelem2  46948  hoidmvlelem3  46949  hoidmvlelem4  46950  ovnhoilem1  46953  ovnhoilem2  46954  ovnlecvr2  46962  ovncvr2  46963  opnvonmbllem2  46985  ovolval4lem1  47001  pimconstlt1  47054  pimgtmnf2  47066  pimdecfgtioc  47067  pimincfltioc  47068  pimdecfgtioo  47069  pimincfltioo  47070  sssmf  47090  incsmflem  47093  smfaddlem1  47115  smfaddlem2  47116  decsmflem  47118  smflimlem1  47123  smflimlem2  47124  smflimlem3  47125  smfrec  47141  smfmullem4  47146  smfdiv  47149  smfsuplem1  47163  smfsuplem3  47165  smfinflem  47169  smflimsuplem1  47172  smflimsuplem7  47178  smfliminflem  47182  sprsymrelfolem1  47846  prmdvdsfmtnof1lem1  47938  prmdvdsfmtnof  47940  perfectALTVlem2  48076  isubgredg  48220  isubgruhgr  48222  isubgrgrim  48283  uhgrimisgrgric  48285  uspgrlimlem1  48342  uspgrlimlem4  48345  uspgrlim  48346  grlimgrtrilem2  48356  oddibas  48527  2zlidl  48594  2zrngbas  48596  2zrng0  48598  isclatd  49336  topclat  49351