Theorem ssrab2 4018

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

Syntax hints:  {crab 3392   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-ss 3907

This theorem is referenced by:  ssrab3  4020  ssrabeq  4022  iinrab2  5006  riinrab  5020  rabelpw  5271  rabexgOLD  5273  frminex  5604  wereu2  5622  predres  6297  frpomin  6298  frpoinsg  6301  ssimaex  6919  f1oresrab  7076  weniso  7305  canth  7317  riotacl  7337  riotassuni  7360  onminesb  7743  onminsb  7744  onintrab  7746  onnminsb  7749  onminex  7752  tfisg  7801  tfis  7802  suppssdm  8124  fnsuppres  8138  oeeulem  8534  nnawordex  8570  pmvalg  8781  fineqvlem  9173  ordtypelem3  9432  ordtypelem4  9433  ordtypelem6  9435  hartogs  9456  card2on  9466  wdom2d  9492  oemapvali  9603  frinsg  9673  tz9.12lem1  9709  tz9.12lem3  9711  rankf  9716  cardf2  9865  cardid2  9875  cardmin2  9921  acni3  9967  dfac2a  10050  cofsmo  10189  coftr  10193  fin2i2  10238  isfin2-2  10239  enfin2i  10241  fin1a2lem11  10330  fin1a2lem12  10331  axdc3lem4  10373  ac6  10400  ondomon  10483  alephval2  10493  pwfseqlem1  10579  pwfseqlem3  10581  wunccl  10665  tskmcl  10762  infm3  12113  uzf  12789  nnwos  12863  supminf  12883  zsupss  12885  rpnnen1lem1  12926  rpnnen1lem3  12927  rpnnen1lem5  12929  ixxf  13306  fzf  13463  flval3  13772  rabssnn0fi  13946  expge0  14058  expge1  14059  hashbclem  14412  01sqrexlem3  15204  rlimrege0  15539  incexc2  15801  bitsf  16394  bitsfzolem  16401  sadadd2lem  16426  sadadd3  16428  sadcl  16429  smupf  16445  smuval2  16449  smupvallem  16450  smucl  16451  smueqlem  16457  lcmcllem  16563  lcmn0cl  16564  lcmledvds  16566  lcmfval  16588  lcmfcllem  16592  lcmfn0cl  16593  lcmfledvds  16599  phicl2  16736  phibnd  16739  hashdvds  16743  phiprmpw  16744  phimullem  16747  eulerth  16751  phisum  16759  odzcllem  16761  odzdvds  16764  prmreclem1  16885  prmreclem2  16886  prmreclem3  16887  prmreclem4  16888  prmreclem5  16889  hashbccl  16972  prmgaplem3  17022  prmgaplem4  17023  prdsds  17425  mrcflem  17570  isacs1i  17621  wunnat  17924  dmcoass  18031  lublecl  18323  lubid  18324  rabsubmgmd  18670  mgmhmeql  18682  issubmd  18772  mhmeql  18792  cntzval  19294  cntzssv  19301  symgsssg  19440  symgfisg  19441  pmtrdifellem4  19452  odfval  19505  odlem1  19508  odlem2  19512  odngen  19550  gexlem1  19552  gexlem2  19555  sylow2alem2  19591  sylow2blem3  19595  oddvdssubg  19828  cyggex2  19870  ablfaclem3  20062  rgspncl  20592  lssacs  20964  lspf  20971  ocvfval  21648  ocvval  21649  dsmmval2  21718  dsmmsubg  21725  asplss  21855  aspsubrg  21857  psrass1lem  21915  psrdi  21946  psrdir  21947  psrass23l  21948  psrass23  21950  resspsrmul  21957  mplbas  21971  mplsubglem  21980  mplsubrglem  21985  mplmonmul  22019  psropprmul  22229  scmatlss  22515  smadiadet  22660  pmatcoe1fsupp  22691  cpmatsubgpmat  22710  fctop  22994  cctop  22996  ppttop  22997  epttop  22999  clscld  23037  neips  23103  neiptopnei  23122  ordtbaslem  23178  ordtuni  23180  ordtcld1  23187  ordtcld2  23188  cnpfval  23224  iscnp2  23229  cmpcov2  23380  cmpsublem  23389  tgcmp  23391  conncompcld  23424  1stcfb  23435  2ndc1stc  23441  2ndcdisj  23446  finlocfin  23510  kgentopon  23528  xkotf  23575  txkgen  23642  xkococnlem  23649  imastopn  23710  kqffn  23715  opnfbas  23832  flimfnfcls  24018  alexsubALT  24041  ptcmplem2  24043  symgtgp  24096  tgpconncompeqg  24102  tgpconncomp  24103  ghmcnp  24105  tsmsfbas  24118  eltsms  24123  utoptop  24224  utopbas  24225  blfvalps  24373  blfps  24396  blf  24397  nmoffn  24701  nmofval  24704  nmogelb  24706  nmolb  24707  nmof  24709  ishtpy  24964  clsocv  25242  rrxnm  25383  rrxbasefi  25402  minveclem3b  25420  minveclem4  25424  ovolcl  25470  ovollb  25471  ovolgelb  25472  ovolge0  25473  ovolshftlem1  25501  ovolshft  25503  ovolscalem1  25505  ovolscalem2  25506  ovolsca  25507  ovolicc2lem3  25511  shftmbl  25530  iundisj  25540  dyadmax  25590  dyadmbllem  25591  opnmbllem  25593  mdegmullem  26068  uc1pval  26130  mon1pval  26132  elqaalem1  26310  elqaalem3  26312  aannenlem2  26320  aalioulem2  26324  radcnvcl  26407  radcnvlt1  26408  radcnvle  26410  ftalem4  27064  ftalem5  27065  efnnfsumcl  27091  isppw  27102  sgmval2  27131  efchtdvds  27147  sqff1o  27170  fsumdvdsdiaglem  27171  fsumdvdsdiag  27172  fsumdvdscom  27173  musum  27179  muinv  27181  sgmmul  27189  ppiub  27192  vmasum  27204  logfac2  27205  perfectlem2  27218  lgsfcl  27293  lgscl  27299  lgsquadlem1  27368  lgsquadlem2  27369  rpvmasumlem  27475  mudivsum  27518  mulogsum  27520  mulog2sumlem2  27523  vmalogdivsum2  27526  logsqvma  27530  logsqvma2  27531  selberglem3  27535  selberg  27536  selberg34r  27559  pntsval2  27564  pntrlog2bndlem1  27565  ltsval2  27645  conway  27796  eqcuts2  27803  cutsun12  27807  cutbdaybnd  27812  cutbdaybnd2  27813  cutbdaylt  27815  bday1  27831  cuteq0  27832  madef  27853  leftssold  27888  rightssold  27889  madebdaylemlrcut  27916  sltsbday  27934  cofcut1  27937  cofcutr  27941  cutlt  27949  precsexlem8  28231  precsexlem11  28234  onssno  28271  oncutlt  28281  oniso  28288  bdayons  28293  bdayn0p1  28386  tglnunirn  28641  tglnssp  28645  incistruhgr  29173  upgrss  29182  upgrn0  29183  upgruhgr  29196  usgrss  29268  uspgrushgr  29271  ushgredgedg  29323  ushgredgedgloop  29325  vtxdun  29575  vtxdginducedm1  29637  wlknwwlksnbij  29981  hashwwlksnext  30007  frcond3  30364  numclwlk1lem2  30465  ocsh  31379  spancl  31432  shsval2i  31483  ococin  31504  chsupid  31508  speccl  31995  hatomistici  32458  chpssati  32459  iundisjf  32685  aciunf1  32762  fpwrelmap  32832  iundisjfi  32895  pwrssmgc  33086  cycpmco2f1  33212  cycpmco2rn  33213  cycpmco2lem1  33214  cycpmco2lem2  33215  cycpmco2lem3  33216  cycpmco2lem4  33217  cycpmco2lem5  33218  cycpmco2lem6  33219  cycpmco2lem7  33220  cycpmco2  33221  fxpss  33254  nsgmgclem  33501  0mplrim  33705  selvply1rhmlemb  33710  selvply1rhm0  33717  extvfvcl  33727  mplmulmvr  33730  evlextv  33733  mplvrpmlem  33734  mplvrpmga  33736  mplvrpmrhm  33738  psrmonmul  33741  esplylem  33757  esplympl  33758  esplymhp  33759  esplyfv1  33760  esplyfv  33761  esplyfval3  33763  esplyfval1  33764  esplyfvaln  33765  constrsuc  33929  locfinreflem  34031  zarclsiin  34062  zarcls  34065  zartopn  34066  esumrnmpt2  34259  esumpinfval  34264  sigagensiga  34332  ldgenpisyslem1  34354  ldgenpisys  34357  measvuni  34405  imambfm  34453  dya2iocuni  34474  omscl  34486  oms0  34488  omsmon  34489  omssubadd  34491  carsgcl  34495  oddpwdc  34545  eulerpartlem1  34558  eulerpartlemt  34562  eulerpartgbij  34563  eulerpartlemmf  34566  eulerpartlemgh  34569  eulerpartlemgs2  34571  ballotlem2  34680  ballotlemfc0  34684  ballotlemfcc  34685  ballotlemfmpn  34686  ballotlemiex  34693  ballotlemsup  34696  ballotlem7  34727  ballotth  34729  reprpmtf1o  34817  breprexplema  34821  hgt750lema  34848  bnj110  35047  bnj1204  35201  bnj1311  35213  fnrelpredd  35279  subfacp1lem6  35420  erdszelem2  35427  connpconn  35470  cvmliftmolem2  35517  cvmliftlem15  35533  cvmlift2lem12  35549  snmlff  35564  satfrnmapom  35605  rankeq1o  36406  finminlem  36553  fnessref  36592  neibastop1  36594  neibastop2lem  36595  weiunlem  36698  weiunse  36703  bj-rabtr  37290  bj-rabtrAUTO  37292  bj-vecssmod  37648  icoreresf  37721  phpreu  37978  fin2so  37981  poimirlem26  38020  poimirlem31  38025  poimirlem32  38026  opnmbllem0  38030  mblfinlem1  38031  mblfinlem2  38032  ismblfin  38035  mbfposadd  38041  cnambfre  38042  cover2  38089  indexa  38107  fdc  38119  sstotbnd2  38148  sstotbnd3  38150  igenidl  38437  prnc  38441  toycom  39472  lkrlss  39594  atlatmstc  39818  atlatle  39819  glbconN  39876  linepsubN  40251  pmapssat  40258  pmaple  40260  pmapsub  40267  paddssat  40313  diass  41541  diaglbN  41554  diaintclN  41557  diassdvaN  41559  docaclN  41623  dibglbN  41665  dibintclN  41666  diclspsn  41693  dihglblem2N  41793  dih1dimatlem  41828  dihglb2  41841  dochval2  41851  dochcl  41852  dochvalr  41856  doch2val2  41863  dochss  41864  dochocss  41865  lclkr  42032  lclkrs  42038  lcdvbase  42092  lcdvbasess  42093  mapdunirnN  42149  aks4d1p4  42571  aks4d1p5  42572  aks4d1p7  42575  aks4d1p8  42579  sticksstones1  42638  aks6d1c6lem2  42663  grpods  42686  unitscyglem1  42687  unitscyglem2  42688  unitscyglem4  42690  mhpind  43051  mhphf  43054  prjcrv0  43090  infdesc  43100  mzpindd  43202  fiphp3d  43271  rencldnfilem  43272  irrapx1  43280  pellexlem3  43283  pellfundre  43333  pellfundge  43334  pellfundlb  43336  pellfundglb  43337  jm2.22  43447  jm2.23  43448  rpnnen3  43484  pwssplit4  43541  pwfi2f1o  43548  hbtlem6  43581  dgraalem  43597  dgraaub  43600  itgocn  43616  onintunirab  43679  nadd2rabord  43837  nadd1rabord  43841  rfovcnvf1od  44455  fsovfd  44463  fsovcnvlem  44464  binomcxplemdvbinom  44804  binomcxplemcvg  44805  binomcxplemnotnn0  44807  uzwo4  45508  disjf1o  45645  icof  45671  allbutfiinf  45870  supminfxr  45914  supminfxr2  45919  fsumsupp0  46030  sumnnodd  46082  fnlimabslt  46129  liminfvalxr  46233  ioodvbdlimc1lem1  46381  dvnprodlem1  46396  dvnprodlem2  46397  stoweidlem14  46464  stoweidlem34  46484  stoweidlem44  46494  stoweidlem50  46500  stoweidlem51  46501  stoweidlem52  46502  stoweidlem57  46507  stoweidlem59  46509  fourierdlem19  46576  fourierdlem20  46577  fourierdlem25  46582  fourierdlem31  46588  fourierdlem37  46594  fourierdlem42  46599  fourierdlem51  46607  fourierdlem54  46610  fourierdlem64  46620  fourierdlem79  46635  elaa2lem  46683  etransclem16  46700  etransclem24  46708  etransclem31  46715  etransclem33  46717  etransclem34  46718  etransclem48  46732  salgencl  46782  salexct  46784  salgenuni  46787  subsaliuncllem  46807  meadjiunlem  46915  caragenss  46954  caratheodory  46978  ovnlecvr  47008  ovnlerp  47012  ovn0lem  47015  ovnsubaddlem1  47020  hoidmv1lelem1  47041  hoidmv1lelem3  47043  hoidmvlelem1  47045  hoidmvlelem2  47046  hoidmvlelem3  47047  hoidmvlelem4  47048  ovnhoilem1  47051  ovnhoilem2  47052  ovnlecvr2  47060  ovncvr2  47061  opnvonmbllem2  47083  ovolval4lem1  47099  pimconstlt1  47152  pimgtmnf2  47164  pimdecfgtioc  47165  pimincfltioc  47166  pimdecfgtioo  47167  pimincfltioo  47168  sssmf  47188  incsmflem  47191  smfaddlem1  47213  smfaddlem2  47214  decsmflem  47216  smflimlem1  47221  smflimlem2  47222  smflimlem3  47223  smfrec  47239  smfmullem4  47244  smfdiv  47247  smfsuplem1  47261  smfsuplem3  47263  smfinflem  47267  smflimsuplem1  47270  smflimsuplem7  47276  smfliminflem  47280  sprsymrelfolem1  47974  prmdvdsfmtnof1lem1  48069  prmdvdsfmtnof  48071  perfectALTVlem2  48220  isubgredg  48364  isubgruhgr  48366  isubgrgrim  48427  uhgrimisgrgric  48429  uspgrlimlem1  48486  uspgrlimlem4  48489  uspgrlim  48490  grlimgrtrilem2  48500  oddibas  48671  2zlidl  48738  2zrngbas  48740  2zrng0  48742  isclatd  49480  topclat  49495