Theorem ssrab2 4089

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

Syntax hints:  {crab 3432   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-ss 3979

This theorem is referenced by:  ssrab3  4091  ssrabeq  4093  iinrab2  5074  riinrab  5088  rabelpw  5341  rabexgOLD  5343  frminex  5667  wereu2  5685  predres  6361  frpomin  6362  frpoinsg  6365  wfisgOLD  6376  ssimaex  6993  f1oresrab  7146  weniso  7373  canth  7384  riotacl  7404  riotassuni  7427  onminesb  7812  onminsb  7813  onintrab  7815  onnminsb  7818  onminex  7821  tfisg  7874  tfis  7875  suppssdm  8200  fnsuppres  8214  oeeulem  8637  nnawordex  8673  pmvalg  8875  fineqvlem  9295  ordtypelem3  9557  ordtypelem4  9558  ordtypelem6  9560  hartogs  9581  card2on  9591  wdom2d  9617  oemapvali  9721  frinsg  9788  tz9.12lem1  9824  tz9.12lem3  9826  rankf  9831  cardf2  9980  cardid2  9990  cardmin2  10036  acni3  10084  dfac2a  10167  cofsmo  10306  coftr  10310  fin2i2  10355  isfin2-2  10356  enfin2i  10358  fin1a2lem11  10447  fin1a2lem12  10448  axdc3lem4  10490  ac6  10517  ondomon  10600  alephval2  10609  pwfseqlem1  10695  pwfseqlem3  10697  wunccl  10781  tskmcl  10878  infm3  12224  uzf  12878  nnwos  12954  supminf  12974  zsupss  12976  rpnnen1lem1  13017  rpnnen1lem3  13018  rpnnen1lem5  13020  ixxf  13393  fzf  13547  flval3  13851  rabssnn0fi  14023  expge0  14135  expge1  14136  hashbclem  14487  01sqrexlem3  15279  rlimrege0  15611  incexc2  15870  bitsf  16460  bitsfzolem  16467  sadadd2lem  16492  sadadd3  16494  sadcl  16495  smupf  16511  smuval2  16515  smupvallem  16516  smucl  16517  smueqlem  16523  lcmcllem  16629  lcmn0cl  16630  lcmledvds  16632  lcmfval  16654  lcmfcllem  16658  lcmfn0cl  16659  lcmfledvds  16665  phicl2  16801  phibnd  16804  hashdvds  16808  phiprmpw  16809  phimullem  16812  eulerth  16816  phisum  16823  odzcllem  16825  odzdvds  16828  prmreclem1  16949  prmreclem2  16950  prmreclem3  16951  prmreclem4  16952  prmreclem5  16953  hashbccl  17036  prmgaplem3  17086  prmgaplem4  17087  prdsds  17510  mrcflem  17650  isacs1i  17701  wunnat  18010  wunnatOLD  18011  dmcoass  18119  lublecl  18418  lubid  18419  rabsubmgmd  18729  mgmhmeql  18741  issubmd  18831  mhmeql  18851  cntzval  19351  cntzssv  19358  symgsssg  19499  symgfisg  19500  pmtrdifellem4  19511  odfval  19564  odlem1  19567  odlem2  19571  odngen  19609  gexlem1  19611  gexlem2  19614  sylow2alem2  19650  sylow2blem3  19654  oddvdssubg  19887  cyggex2  19929  ablfaclem3  20121  rgspncl  20629  lssacs  20982  lspf  20989  ocvfval  21701  ocvval  21702  dsmmval2  21773  dsmmsubg  21780  asplss  21911  aspsubrg  21913  psrass1lem  21969  psrdi  22002  psrdir  22003  psrass23l  22004  psrass23  22006  resspsrmul  22013  mplbas  22027  mplsubglem  22036  mplsubrglem  22041  mplmonmul  22071  psropprmul  22254  scmatlss  22546  smadiadet  22691  pmatcoe1fsupp  22722  cpmatsubgpmat  22741  fctop  23026  cctop  23028  ppttop  23029  epttop  23031  clscld  23070  neips  23136  neiptopnei  23155  ordtbaslem  23211  ordtuni  23213  ordtcld1  23220  ordtcld2  23221  cnpfval  23257  iscnp2  23262  cmpcov2  23413  cmpsublem  23422  tgcmp  23424  conncompcld  23457  1stcfb  23468  2ndc1stc  23474  2ndcdisj  23479  finlocfin  23543  kgentopon  23561  xkotf  23608  txkgen  23675  xkococnlem  23682  imastopn  23743  kqffn  23748  opnfbas  23865  flimfnfcls  24051  alexsubALT  24074  ptcmplem2  24076  symgtgp  24129  tgpconncompeqg  24135  tgpconncomp  24136  ghmcnp  24138  tsmsfbas  24151  eltsms  24156  utoptop  24258  utopbas  24259  blfvalps  24408  blfps  24431  blf  24432  nmoffn  24747  nmofval  24750  nmogelb  24752  nmolb  24753  nmof  24755  ishtpy  25017  clsocv  25297  rrxnm  25438  rrxbasefi  25457  minveclem3b  25475  minveclem4  25479  ovolcl  25526  ovollb  25527  ovolgelb  25528  ovolge0  25529  ovolshftlem1  25557  ovolshft  25559  ovolscalem1  25561  ovolscalem2  25562  ovolsca  25563  ovolicc2lem3  25567  shftmbl  25586  iundisj  25596  dyadmax  25646  dyadmbllem  25647  opnmbllem  25649  mdegmullem  26131  uc1pval  26193  mon1pval  26195  elqaalem1  26375  elqaalem3  26377  aannenlem2  26385  aalioulem2  26389  radcnvcl  26474  radcnvlt1  26475  radcnvle  26477  ftalem4  27133  ftalem5  27134  efnnfsumcl  27160  isppw  27171  sgmval2  27200  efchtdvds  27216  sqff1o  27239  fsumdvdsdiaglem  27240  fsumdvdsdiag  27241  fsumdvdscom  27242  musum  27248  muinv  27250  sgmmul  27259  ppiub  27262  vmasum  27274  logfac2  27275  perfectlem2  27288  lgsfcl  27363  lgscl  27369  lgsquadlem1  27438  lgsquadlem2  27439  rpvmasumlem  27545  mudivsum  27588  mulogsum  27590  mulog2sumlem2  27593  vmalogdivsum2  27596  logsqvma  27600  logsqvma2  27601  selberglem3  27605  selberg  27606  selberg34r  27629  pntsval2  27634  pntrlog2bndlem1  27635  sltval2  27715  conway  27858  eqscut2  27865  scutun12  27869  scutbdaybnd  27874  scutbdaybnd2  27875  scutbdaylt  27877  bday1s  27890  cuteq0  27891  madef  27909  leftssold  27931  rightssold  27932  madebdaylemlrcut  27951  cofcut1  27968  cofcutr  27972  cutlt  27980  precsexlem8  28252  precsexlem11  28255  onssno  28291  tglnunirn  28570  tglnssp  28574  incistruhgr  29110  upgrss  29119  upgrn0  29120  upgruhgr  29133  usgrss  29205  uspgrushgr  29208  ushgredgedg  29260  ushgredgedgloop  29262  vtxdun  29513  vtxdginducedm1  29575  wlknwwlksnbij  29917  hashwwlksnext  29943  frcond3  30297  numclwlk1lem2  30398  ocsh  31311  spancl  31364  shsval2i  31415  ococin  31436  chsupid  31440  speccl  31927  hatomistici  32390  chpssati  32391  iundisjf  32608  aciunf1  32679  fpwrelmap  32750  iundisjfi  32803  pwrssmgc  32974  cycpmco2f1  33126  cycpmco2rn  33127  cycpmco2lem1  33128  cycpmco2lem2  33129  cycpmco2lem3  33130  cycpmco2lem4  33131  cycpmco2lem5  33132  cycpmco2lem6  33133  cycpmco2lem7  33134  cycpmco2  33135  nsgmgclem  33418  constrsuc  33742  locfinreflem  33800  zarclsiin  33831  zarcls  33834  zartopn  33835  esumrnmpt2  34048  esumpinfval  34053  sigagensiga  34121  ldgenpisyslem1  34143  ldgenpisys  34146  measvuni  34194  imambfm  34243  dya2iocuni  34264  omscl  34276  oms0  34278  omsmon  34279  omssubadd  34281  carsgcl  34285  oddpwdc  34335  eulerpartlem1  34348  eulerpartlemt  34352  eulerpartgbij  34353  eulerpartlemmf  34356  eulerpartlemgh  34359  eulerpartlemgs2  34361  ballotlem2  34469  ballotlemfc0  34473  ballotlemfcc  34474  ballotlemfmpn  34475  ballotlemiex  34482  ballotlemsup  34485  ballotlem7  34516  ballotth  34518  reprpmtf1o  34619  breprexplema  34623  hgt750lema  34650  bnj110  34850  bnj1204  35004  bnj1311  35016  fnrelpredd  35081  subfacp1lem6  35169  erdszelem2  35176  connpconn  35219  cvmliftmolem2  35266  cvmliftlem15  35282  cvmlift2lem12  35298  snmlff  35313  satfrnmapom  35354  rankeq1o  36152  finminlem  36300  fnessref  36339  neibastop1  36341  neibastop2lem  36342  weiunlem2  36445  weiunse  36450  bj-rabtr  36912  bj-rabtrAUTO  36914  bj-vecssmod  37263  icoreresf  37334  phpreu  37590  fin2so  37593  poimirlem26  37632  poimirlem31  37637  poimirlem32  37638  opnmbllem0  37642  mblfinlem1  37643  mblfinlem2  37644  ismblfin  37647  mbfposadd  37653  cnambfre  37654  cover2  37701  indexa  37719  fdc  37731  sstotbnd2  37760  sstotbnd3  37762  igenidl  38049  prnc  38053  toycom  38954  lkrlss  39076  atlatmstc  39300  atlatle  39301  glbconN  39358  glbconNOLD  39359  linepsubN  39734  pmapssat  39741  pmaple  39743  pmapsub  39750  paddssat  39796  diass  41024  diaglbN  41037  diaintclN  41040  diassdvaN  41042  docaclN  41106  dibglbN  41148  dibintclN  41149  diclspsn  41176  dihglblem2N  41276  dih1dimatlem  41311  dihglb2  41324  dochval2  41334  dochcl  41335  dochvalr  41339  doch2val2  41346  dochss  41347  dochocss  41348  lclkr  41515  lclkrs  41521  lcdvbase  41575  lcdvbasess  41576  mapdunirnN  41632  aks4d1p4  42060  aks4d1p5  42061  aks4d1p7  42064  aks4d1p8  42068  sticksstones1  42127  aks6d1c6lem2  42152  grpods  42175  unitscyglem1  42176  unitscyglem2  42177  unitscyglem4  42179  mhpind  42580  mhphf  42583  prjcrv0  42619  infdesc  42629  mzpindd  42733  fiphp3d  42806  rencldnfilem  42807  irrapx1  42815  pellexlem3  42818  pellfundre  42868  pellfundge  42869  pellfundlb  42871  pellfundglb  42872  jm2.22  42983  jm2.23  42984  rpnnen3  43020  pwssplit4  43077  pwfi2f1o  43084  hbtlem6  43117  dgraalem  43133  dgraaub  43136  itgocn  43152  onintunirab  43215  nadd2rabord  43374  nadd1rabord  43378  rfovcnvf1od  43993  fsovfd  44001  fsovcnvlem  44002  binomcxplemdvbinom  44348  binomcxplemcvg  44349  binomcxplemnotnn0  44351  uzwo4  44992  disjf1o  45133  icof  45161  allbutfiinf  45369  supminfxr  45413  supminfxr2  45418  fsumsupp0  45533  sumnnodd  45585  fnlimabslt  45634  liminfvalxr  45738  ioodvbdlimc1lem1  45886  dvnprodlem1  45901  dvnprodlem2  45902  stoweidlem14  45969  stoweidlem34  45989  stoweidlem44  45999  stoweidlem50  46005  stoweidlem51  46006  stoweidlem52  46007  stoweidlem57  46012  stoweidlem59  46014  fourierdlem19  46081  fourierdlem20  46082  fourierdlem25  46087  fourierdlem31  46093  fourierdlem37  46099  fourierdlem42  46104  fourierdlem51  46112  fourierdlem54  46115  fourierdlem64  46125  fourierdlem79  46140  elaa2lem  46188  etransclem16  46205  etransclem24  46213  etransclem31  46220  etransclem33  46222  etransclem34  46223  etransclem48  46237  salgencl  46287  salexct  46289  salgenuni  46292  subsaliuncllem  46312  meadjiunlem  46420  caragenss  46459  caratheodory  46483  ovnlecvr  46513  ovnlerp  46517  ovn0lem  46520  ovnsubaddlem1  46525  hoidmv1lelem1  46546  hoidmv1lelem3  46548  hoidmvlelem1  46550  hoidmvlelem2  46551  hoidmvlelem3  46552  hoidmvlelem4  46553  ovnhoilem1  46556  ovnhoilem2  46557  ovnlecvr2  46565  ovncvr2  46566  opnvonmbllem2  46588  ovolval4lem1  46604  pimconstlt1  46657  pimiooltgt  46665  pimgtmnf2  46669  pimdecfgtioc  46670  pimincfltioc  46671  pimdecfgtioo  46672  pimincfltioo  46673  sssmf  46693  incsmflem  46696  smfaddlem1  46718  smfaddlem2  46719  decsmflem  46721  smflimlem1  46726  smflimlem2  46727  smflimlem3  46728  smfrec  46744  smfmullem4  46749  smfdiv  46752  smfsuplem1  46766  smfsuplem3  46768  smfinflem  46772  smflimsuplem1  46775  smflimsuplem7  46781  smfliminflem  46785  sprsymrelfolem1  47416  prmdvdsfmtnof1lem1  47508  prmdvdsfmtnof  47510  perfectALTVlem2  47646  isubgredg  47789  isubgruhgr  47791  isubgrgrim  47834  uhgrimisgrgric  47836  uspgrlimlem1  47890  uspgrlimlem4  47893  uspgrlim  47894  grlimgrtrilem2  47897  oddibas  48016  2zlidl  48083  2zrngbas  48085  2zrng0  48087  isclatd  48771  topclat  48786