Theorem ssrab2 4029

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

Syntax hints:  {crab 3396   ⊆ wss 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-ss 3915

This theorem is referenced by:  ssrab3  4031  ssrabeq  4033  iinrab2  5020  riinrab  5034  rabelpw  5276  rabexgOLD  5278  frminex  5598  wereu2  5616  predres  6291  frpomin  6292  frpoinsg  6295  ssimaex  6913  f1oresrab  7066  weniso  7294  canth  7306  riotacl  7326  riotassuni  7349  onminesb  7732  onminsb  7733  onintrab  7735  onnminsb  7738  onminex  7741  tfisg  7790  tfis  7791  suppssdm  8113  fnsuppres  8127  oeeulem  8522  nnawordex  8558  pmvalg  8767  fineqvlem  9157  ordtypelem3  9413  ordtypelem4  9414  ordtypelem6  9416  hartogs  9437  card2on  9447  wdom2d  9473  oemapvali  9581  frinsg  9651  tz9.12lem1  9687  tz9.12lem3  9689  rankf  9694  cardf2  9843  cardid2  9853  cardmin2  9899  acni3  9945  dfac2a  10028  cofsmo  10167  coftr  10171  fin2i2  10216  isfin2-2  10217  enfin2i  10219  fin1a2lem11  10308  fin1a2lem12  10309  axdc3lem4  10351  ac6  10378  ondomon  10461  alephval2  10470  pwfseqlem1  10556  pwfseqlem3  10558  wunccl  10642  tskmcl  10739  infm3  12088  uzf  12741  nnwos  12815  supminf  12835  zsupss  12837  rpnnen1lem1  12878  rpnnen1lem3  12879  rpnnen1lem5  12881  ixxf  13257  fzf  13413  flval3  13721  rabssnn0fi  13895  expge0  14007  expge1  14008  hashbclem  14361  01sqrexlem3  15153  rlimrege0  15488  incexc2  15747  bitsf  16340  bitsfzolem  16347  sadadd2lem  16372  sadadd3  16374  sadcl  16375  smupf  16391  smuval2  16395  smupvallem  16396  smucl  16397  smueqlem  16403  lcmcllem  16509  lcmn0cl  16510  lcmledvds  16512  lcmfval  16534  lcmfcllem  16538  lcmfn0cl  16539  lcmfledvds  16545  phicl2  16681  phibnd  16684  hashdvds  16688  phiprmpw  16689  phimullem  16692  eulerth  16696  phisum  16704  odzcllem  16706  odzdvds  16709  prmreclem1  16830  prmreclem2  16831  prmreclem3  16832  prmreclem4  16833  prmreclem5  16834  hashbccl  16917  prmgaplem3  16967  prmgaplem4  16968  prdsds  17370  mrcflem  17514  isacs1i  17565  wunnat  17868  dmcoass  17975  lublecl  18267  lubid  18268  rabsubmgmd  18614  mgmhmeql  18626  issubmd  18716  mhmeql  18736  cntzval  19235  cntzssv  19242  symgsssg  19381  symgfisg  19382  pmtrdifellem4  19393  odfval  19446  odlem1  19449  odlem2  19453  odngen  19491  gexlem1  19493  gexlem2  19496  sylow2alem2  19532  sylow2blem3  19536  oddvdssubg  19769  cyggex2  19811  ablfaclem3  20003  rgspncl  20530  lssacs  20902  lspf  20909  ocvfval  21605  ocvval  21606  dsmmval2  21675  dsmmsubg  21682  asplss  21813  aspsubrg  21815  psrass1lem  21871  psrdi  21903  psrdir  21904  psrass23l  21905  psrass23  21907  resspsrmul  21914  mplbas  21928  mplsubglem  21937  mplsubrglem  21942  mplmonmul  21972  psropprmul  22151  scmatlss  22441  smadiadet  22586  pmatcoe1fsupp  22617  cpmatsubgpmat  22636  fctop  22920  cctop  22922  ppttop  22923  epttop  22925  clscld  22963  neips  23029  neiptopnei  23048  ordtbaslem  23104  ordtuni  23106  ordtcld1  23113  ordtcld2  23114  cnpfval  23150  iscnp2  23155  cmpcov2  23306  cmpsublem  23315  tgcmp  23317  conncompcld  23350  1stcfb  23361  2ndc1stc  23367  2ndcdisj  23372  finlocfin  23436  kgentopon  23454  xkotf  23501  txkgen  23568  xkococnlem  23575  imastopn  23636  kqffn  23641  opnfbas  23758  flimfnfcls  23944  alexsubALT  23967  ptcmplem2  23969  symgtgp  24022  tgpconncompeqg  24028  tgpconncomp  24029  ghmcnp  24031  tsmsfbas  24044  eltsms  24049  utoptop  24150  utopbas  24151  blfvalps  24299  blfps  24322  blf  24323  nmoffn  24627  nmofval  24630  nmogelb  24632  nmolb  24633  nmof  24635  ishtpy  24899  clsocv  25178  rrxnm  25319  rrxbasefi  25338  minveclem3b  25356  minveclem4  25360  ovolcl  25407  ovollb  25408  ovolgelb  25409  ovolge0  25410  ovolshftlem1  25438  ovolshft  25440  ovolscalem1  25442  ovolscalem2  25443  ovolsca  25444  ovolicc2lem3  25448  shftmbl  25467  iundisj  25477  dyadmax  25527  dyadmbllem  25528  opnmbllem  25530  mdegmullem  26011  uc1pval  26073  mon1pval  26075  elqaalem1  26255  elqaalem3  26257  aannenlem2  26265  aalioulem2  26269  radcnvcl  26354  radcnvlt1  26355  radcnvle  26357  ftalem4  27014  ftalem5  27015  efnnfsumcl  27041  isppw  27052  sgmval2  27081  efchtdvds  27097  sqff1o  27120  fsumdvdsdiaglem  27121  fsumdvdsdiag  27122  fsumdvdscom  27123  musum  27129  muinv  27131  sgmmul  27140  ppiub  27143  vmasum  27155  logfac2  27156  perfectlem2  27169  lgsfcl  27244  lgscl  27250  lgsquadlem1  27319  lgsquadlem2  27320  rpvmasumlem  27426  mudivsum  27469  mulogsum  27471  mulog2sumlem2  27474  vmalogdivsum2  27477  logsqvma  27481  logsqvma2  27482  selberglem3  27486  selberg  27487  selberg34r  27510  pntsval2  27515  pntrlog2bndlem1  27516  sltval2  27596  conway  27741  eqscut2  27748  scutun12  27752  scutbdaybnd  27757  scutbdaybnd2  27758  scutbdaylt  27760  bday1s  27776  cuteq0  27777  madef  27798  leftssold  27825  rightssold  27826  madebdaylemlrcut  27845  cofcut1  27865  cofcutr  27869  cutlt  27877  precsexlem8  28153  precsexlem11  28156  onssno  28192  onscutlt  28202  onsiso  28206  bdayon  28210  bdayn0p1  28295  tglnunirn  28527  tglnssp  28531  incistruhgr  29059  upgrss  29068  upgrn0  29069  upgruhgr  29082  usgrss  29154  uspgrushgr  29157  ushgredgedg  29209  ushgredgedgloop  29211  vtxdun  29462  vtxdginducedm1  29524  wlknwwlksnbij  29868  hashwwlksnext  29894  frcond3  30251  numclwlk1lem2  30352  ocsh  31265  spancl  31318  shsval2i  31369  ococin  31390  chsupid  31394  speccl  31881  hatomistici  32344  chpssati  32345  iundisjf  32571  aciunf1  32647  fpwrelmap  32720  iundisjfi  32783  pwrssmgc  32988  cycpmco2f1  33100  cycpmco2rn  33101  cycpmco2lem1  33102  cycpmco2lem2  33103  cycpmco2lem3  33104  cycpmco2lem4  33105  cycpmco2lem5  33106  cycpmco2lem6  33107  cycpmco2lem7  33108  cycpmco2  33109  fxpss  33142  nsgmgclem  33383  extvfvcl  33587  mplmulmvr  33590  mplvrpmlem  33591  mplvrpmga  33593  mplvrpmrhm  33595  esplylem  33606  esplympl  33607  esplymhp  33608  esplyfv1  33609  esplyfv  33610  esplyfval3  33612  constrsuc  33772  locfinreflem  33874  zarclsiin  33905  zarcls  33908  zartopn  33909  esumrnmpt2  34102  esumpinfval  34107  sigagensiga  34175  ldgenpisyslem1  34197  ldgenpisys  34200  measvuni  34248  imambfm  34296  dya2iocuni  34317  omscl  34329  oms0  34331  omsmon  34332  omssubadd  34334  carsgcl  34338  oddpwdc  34388  eulerpartlem1  34401  eulerpartlemt  34405  eulerpartgbij  34406  eulerpartlemmf  34409  eulerpartlemgh  34412  eulerpartlemgs2  34414  ballotlem2  34523  ballotlemfc0  34527  ballotlemfcc  34528  ballotlemfmpn  34529  ballotlemiex  34536  ballotlemsup  34539  ballotlem7  34570  ballotth  34572  reprpmtf1o  34660  breprexplema  34664  hgt750lema  34691  bnj110  34891  bnj1204  35045  bnj1311  35057  fnrelpredd  35123  subfacp1lem6  35250  erdszelem2  35257  connpconn  35300  cvmliftmolem2  35347  cvmliftlem15  35363  cvmlift2lem12  35379  snmlff  35394  satfrnmapom  35435  rankeq1o  36236  finminlem  36383  fnessref  36422  neibastop1  36424  neibastop2lem  36425  weiunlem2  36528  weiunse  36533  bj-rabtr  36995  bj-rabtrAUTO  36997  bj-vecssmod  37346  icoreresf  37417  phpreu  37665  fin2so  37668  poimirlem26  37707  poimirlem31  37712  poimirlem32  37713  opnmbllem0  37717  mblfinlem1  37718  mblfinlem2  37719  ismblfin  37722  mbfposadd  37728  cnambfre  37729  cover2  37776  indexa  37794  fdc  37806  sstotbnd2  37835  sstotbnd3  37837  igenidl  38124  prnc  38128  toycom  39093  lkrlss  39215  atlatmstc  39439  atlatle  39440  glbconN  39497  linepsubN  39872  pmapssat  39879  pmaple  39881  pmapsub  39888  paddssat  39934  diass  41162  diaglbN  41175  diaintclN  41178  diassdvaN  41180  docaclN  41244  dibglbN  41286  dibintclN  41287  diclspsn  41314  dihglblem2N  41414  dih1dimatlem  41449  dihglb2  41462  dochval2  41472  dochcl  41473  dochvalr  41477  doch2val2  41484  dochss  41485  dochocss  41486  lclkr  41653  lclkrs  41659  lcdvbase  41713  lcdvbasess  41714  mapdunirnN  41770  aks4d1p4  42193  aks4d1p5  42194  aks4d1p7  42197  aks4d1p8  42201  sticksstones1  42260  aks6d1c6lem2  42285  grpods  42308  unitscyglem1  42309  unitscyglem2  42310  unitscyglem4  42312  mhpind  42713  mhphf  42716  prjcrv0  42752  infdesc  42762  mzpindd  42864  fiphp3d  42937  rencldnfilem  42938  irrapx1  42946  pellexlem3  42949  pellfundre  42999  pellfundge  43000  pellfundlb  43002  pellfundglb  43003  jm2.22  43113  jm2.23  43114  rpnnen3  43150  pwssplit4  43207  pwfi2f1o  43214  hbtlem6  43247  dgraalem  43263  dgraaub  43266  itgocn  43282  onintunirab  43345  nadd2rabord  43503  nadd1rabord  43507  rfovcnvf1od  44122  fsovfd  44130  fsovcnvlem  44131  binomcxplemdvbinom  44471  binomcxplemcvg  44472  binomcxplemnotnn0  44474  uzwo4  45175  disjf1o  45313  icof  45341  allbutfiinf  45543  supminfxr  45587  supminfxr2  45592  fsumsupp0  45703  sumnnodd  45755  fnlimabslt  45802  liminfvalxr  45906  ioodvbdlimc1lem1  46054  dvnprodlem1  46069  dvnprodlem2  46070  stoweidlem14  46137  stoweidlem34  46157  stoweidlem44  46167  stoweidlem50  46173  stoweidlem51  46174  stoweidlem52  46175  stoweidlem57  46180  stoweidlem59  46182  fourierdlem19  46249  fourierdlem20  46250  fourierdlem25  46255  fourierdlem31  46261  fourierdlem37  46267  fourierdlem42  46272  fourierdlem51  46280  fourierdlem54  46283  fourierdlem64  46293  fourierdlem79  46308  elaa2lem  46356  etransclem16  46373  etransclem24  46381  etransclem31  46388  etransclem33  46390  etransclem34  46391  etransclem48  46405  salgencl  46455  salexct  46457  salgenuni  46460  subsaliuncllem  46480  meadjiunlem  46588  caragenss  46627  caratheodory  46651  ovnlecvr  46681  ovnlerp  46685  ovn0lem  46688  ovnsubaddlem1  46693  hoidmv1lelem1  46714  hoidmv1lelem3  46716  hoidmvlelem1  46718  hoidmvlelem2  46719  hoidmvlelem3  46720  hoidmvlelem4  46721  ovnhoilem1  46724  ovnhoilem2  46725  ovnlecvr2  46733  ovncvr2  46734  opnvonmbllem2  46756  ovolval4lem1  46772  pimconstlt1  46825  pimgtmnf2  46837  pimdecfgtioc  46838  pimincfltioc  46839  pimdecfgtioo  46840  pimincfltioo  46841  sssmf  46861  incsmflem  46864  smfaddlem1  46886  smfaddlem2  46887  decsmflem  46889  smflimlem1  46894  smflimlem2  46895  smflimlem3  46896  smfrec  46912  smfmullem4  46917  smfdiv  46920  smfsuplem1  46934  smfsuplem3  46936  smfinflem  46940  smflimsuplem1  46943  smflimsuplem7  46949  smfliminflem  46953  sprsymrelfolem1  47617  prmdvdsfmtnof1lem1  47709  prmdvdsfmtnof  47711  perfectALTVlem2  47847  isubgredg  47991  isubgruhgr  47993  isubgrgrim  48054  uhgrimisgrgric  48056  uspgrlimlem1  48113  uspgrlimlem4  48116  uspgrlim  48117  grlimgrtrilem2  48127  oddibas  48298  2zlidl  48365  2zrngbas  48367  2zrng0  48369  isclatd  49108  topclat  49123