Theorem ssrab2 4078

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

Syntax hints:  {crab 3430   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-in 3956  df-ss 3966

This theorem is referenced by:  ssrab3  4081  ssrabeq  4083  iinrab2  5074  riinrab  5088  rabexg  5332  pwnss  5350  rabelpw  5353  frminex  5657  wereu2  5674  predres  6341  frpomin  6342  frpoinsg  6345  wfisgOLD  6356  ssimaex  6977  f1oresrab  7128  weniso  7355  canth  7366  riotacl  7387  riotassuni  7410  onminesb  7785  onminsb  7786  onintrab  7788  onnminsb  7791  onminex  7794  tfisg  7847  tfis  7848  suppssdm  8166  fnsuppres  8180  oeeulem  8605  nnawordex  8641  pmvalg  8835  fineqvlem  9266  ordtypelem3  9519  ordtypelem4  9520  ordtypelem6  9522  hartogs  9543  card2on  9553  wdom2d  9579  oemapvali  9683  frinsg  9750  tz9.12lem1  9786  tz9.12lem3  9788  rankf  9793  cardf2  9942  cardid2  9952  cardmin2  9998  acni3  10046  dfac2a  10128  cofsmo  10268  coftr  10272  fin2i2  10317  isfin2-2  10318  enfin2i  10320  fin1a2lem11  10409  fin1a2lem12  10410  axdc3lem4  10452  ac6  10479  ondomon  10562  alephval2  10571  pwfseqlem1  10657  pwfseqlem3  10659  wunccl  10743  tskmcl  10840  infm3  12179  uzf  12831  nnwos  12905  supminf  12925  zsupss  12927  rpnnen1lem1  12968  rpnnen1lem3  12969  rpnnen1lem5  12971  ixxf  13340  fzf  13494  flval3  13786  rabssnn0fi  13957  expge0  14070  expge1  14071  hashbclem  14417  01sqrexlem3  15197  rlimrege0  15529  incexc2  15790  bitsf  16374  bitsfzolem  16381  sadadd2lem  16406  sadadd3  16408  sadcl  16409  smupf  16425  smuval2  16429  smupvallem  16430  smucl  16431  smueqlem  16437  lcmcllem  16539  lcmn0cl  16540  lcmledvds  16542  lcmfval  16564  lcmfcllem  16568  lcmfn0cl  16569  lcmfledvds  16575  phicl2  16707  phibnd  16710  hashdvds  16714  phiprmpw  16715  phimullem  16718  eulerth  16722  phisum  16729  odzcllem  16731  odzdvds  16734  prmreclem1  16855  prmreclem2  16856  prmreclem3  16857  prmreclem4  16858  prmreclem5  16859  hashbccl  16942  prmgaplem3  16992  prmgaplem4  16993  prdsds  17416  mrcflem  17556  isacs1i  17607  wunnat  17913  wunnatOLD  17914  dmcoass  18022  lublecl  18320  lubid  18321  rabsubmgmd  18631  mgmhmeql  18643  issubmd  18725  mhmeql  18745  cntzval  19228  cntzssv  19235  symgsssg  19378  symgfisg  19379  pmtrdifellem4  19390  odfval  19443  odlem1  19446  odlem2  19450  odngen  19488  gexlem1  19490  gexlem2  19493  sylow2alem2  19529  sylow2blem3  19533  oddvdssubg  19766  cyggex2  19808  ablfaclem3  20000  lssacs  20724  lspf  20731  ocvfval  21440  ocvval  21441  dsmmval2  21512  dsmmsubg  21519  asplss  21649  aspsubrg  21651  psrass1lemOLD  21714  psrass1lem  21717  psrdi  21747  psrdir  21748  psrass23l  21749  psrass23  21751  resspsrmul  21758  mplbas  21770  mplsubglem  21779  mplsubrglem  21784  mplmonmul  21812  psropprmul  21982  scmatlss  22249  smadiadet  22394  pmatcoe1fsupp  22425  cpmatsubgpmat  22444  fctop  22729  cctop  22731  ppttop  22732  epttop  22734  clscld  22773  neips  22839  neiptopnei  22858  ordtbaslem  22914  ordtuni  22916  ordtcld1  22923  ordtcld2  22924  cnpfval  22960  iscnp2  22965  cmpcov2  23116  cmpsublem  23125  tgcmp  23127  conncompcld  23160  1stcfb  23171  2ndc1stc  23177  2ndcdisj  23182  finlocfin  23246  kgentopon  23264  xkotf  23311  txkgen  23378  xkococnlem  23385  imastopn  23446  kqffn  23451  opnfbas  23568  flimfnfcls  23754  alexsubALT  23777  ptcmplem2  23779  symgtgp  23832  tgpconncompeqg  23838  tgpconncomp  23839  ghmcnp  23841  tsmsfbas  23854  eltsms  23859  utoptop  23961  utopbas  23962  blfvalps  24111  blfps  24134  blf  24135  nmoffn  24450  nmofval  24453  nmogelb  24455  nmolb  24456  nmof  24458  ishtpy  24720  clsocv  25000  rrxnm  25141  rrxbasefi  25160  minveclem3b  25178  minveclem4  25182  ovolcl  25229  ovollb  25230  ovolgelb  25231  ovolge0  25232  ovolshftlem1  25260  ovolshft  25262  ovolscalem1  25264  ovolscalem2  25265  ovolsca  25266  ovolicc2lem3  25270  shftmbl  25289  iundisj  25299  dyadmax  25349  dyadmbllem  25350  opnmbllem  25352  mdegmullem  25830  uc1pval  25891  mon1pval  25893  elqaalem1  26066  elqaalem3  26068  aannenlem2  26076  aalioulem2  26080  radcnvcl  26163  radcnvlt1  26164  radcnvle  26166  ftalem4  26814  ftalem5  26815  efnnfsumcl  26841  isppw  26852  sgmval2  26881  efchtdvds  26897  sqff1o  26920  fsumdvdsdiaglem  26921  fsumdvdsdiag  26922  fsumdvdscom  26923  musum  26929  muinv  26931  sgmmul  26938  ppiub  26941  vmasum  26953  logfac2  26954  perfectlem2  26967  lgsfcl  27042  lgscl  27048  lgsquadlem1  27117  lgsquadlem2  27118  rpvmasumlem  27224  mudivsum  27267  mulogsum  27269  mulog2sumlem2  27272  vmalogdivsum2  27275  logsqvma  27279  logsqvma2  27280  selberglem3  27284  selberg  27285  selberg34r  27308  pntsval2  27313  pntrlog2bndlem1  27314  sltval2  27393  conway  27535  eqscut2  27542  scutun12  27546  scutbdaybnd  27551  scutbdaybnd2  27552  scutbdaylt  27554  bday1s  27567  cuteq0  27568  madef  27586  leftssold  27608  rightssold  27609  madebdaylemlrcut  27628  cofcut1  27643  cofcutr  27647  cutlt  27655  precsexlem8  27897  precsexlem11  27900  onssno  27918  tglnunirn  28064  tglnssp  28068  incistruhgr  28604  upgrss  28613  upgrn0  28614  upgruhgr  28627  usgrss  28699  uspgrushgr  28700  ushgredgedg  28751  ushgredgedgloop  28753  vtxdun  29003  vtxdginducedm1  29065  wlknwwlksnbij  29407  hashwwlksnext  29433  frcond3  29787  numclwlk1lem2  29888  ocsh  30801  spancl  30854  shsval2i  30905  ococin  30926  chsupid  30930  speccl  31417  hatomistici  31880  chpssati  31881  iundisjf  32085  aciunf1  32153  fpwrelmap  32223  iundisjfi  32272  pwrssmgc  32435  cycpmco2f1  32551  cycpmco2rn  32552  cycpmco2lem1  32553  cycpmco2lem2  32554  cycpmco2lem3  32555  cycpmco2lem4  32556  cycpmco2lem5  32557  cycpmco2lem6  32558  cycpmco2lem7  32559  cycpmco2  32560  nsgmgclem  32794  locfinreflem  33116  zarclsiin  33147  zarcls  33150  zartopn  33151  esumrnmpt2  33362  esumpinfval  33367  sigagensiga  33435  ldgenpisyslem1  33457  ldgenpisys  33460  measvuni  33508  imambfm  33557  dya2iocuni  33578  omscl  33590  oms0  33592  omsmon  33593  omssubadd  33595  carsgcl  33599  oddpwdc  33649  eulerpartlem1  33662  eulerpartlemt  33666  eulerpartgbij  33667  eulerpartlemmf  33670  eulerpartlemgh  33673  eulerpartlemgs2  33675  ballotlem2  33783  ballotlemfc0  33787  ballotlemfcc  33788  ballotlemfmpn  33789  ballotlemiex  33796  ballotlemsup  33799  ballotlem7  33830  ballotth  33832  reprpmtf1o  33934  breprexplema  33938  hgt750lema  33965  bnj110  34165  bnj1204  34319  bnj1311  34331  fnrelpredd  34388  subfacp1lem6  34472  erdszelem2  34479  connpconn  34522  cvmliftmolem2  34569  cvmliftlem15  34585  cvmlift2lem12  34601  snmlff  34616  satfrnmapom  34657  rankeq1o  35445  finminlem  35508  fnessref  35547  neibastop1  35549  neibastop2lem  35550  bj-rabtr  36115  bj-rabtrAUTO  36117  bj-vecssmod  36467  icoreresf  36538  phpreu  36777  fin2so  36780  poimirlem26  36819  poimirlem31  36824  poimirlem32  36825  opnmbllem0  36829  mblfinlem1  36830  mblfinlem2  36831  ismblfin  36834  mbfposadd  36840  cnambfre  36841  cover2  36888  indexa  36906  fdc  36918  sstotbnd2  36947  sstotbnd3  36949  igenidl  37236  prnc  37240  toycom  38148  lkrlss  38270  atlatmstc  38494  atlatle  38495  glbconN  38552  glbconNOLD  38553  linepsubN  38928  pmapssat  38935  pmaple  38937  pmapsub  38944  paddssat  38990  diass  40218  diaglbN  40231  diaintclN  40234  diassdvaN  40236  docaclN  40300  dibglbN  40342  dibintclN  40343  diclspsn  40370  dihglblem2N  40470  dih1dimatlem  40505  dihglb2  40518  dochval2  40528  dochcl  40529  dochvalr  40533  doch2val2  40540  dochss  40541  dochocss  40542  lclkr  40709  lclkrs  40715  lcdvbase  40769  lcdvbasess  40770  mapdunirnN  40826  aks4d1p4  41252  aks4d1p5  41253  aks4d1p7  41256  aks4d1p8  41260  sticksstones1  41270  mhpind  41470  mhphf  41473  prjcrv0  41679  infdesc  41689  mzpindd  41788  fiphp3d  41861  rencldnfilem  41862  irrapx1  41870  pellexlem3  41873  pellfundre  41923  pellfundge  41924  pellfundlb  41926  pellfundglb  41927  jm2.22  42038  jm2.23  42039  rpnnen3  42075  pwssplit4  42135  pwfi2f1o  42142  hbtlem6  42175  dgraalem  42191  dgraaub  42194  itgocn  42210  rgspncl  42215  onintunirab  42280  nadd2rabord  42439  nadd1rabord  42443  rfovcnvf1od  43059  fsovfd  43067  fsovcnvlem  43068  binomcxplemdvbinom  43416  binomcxplemcvg  43417  binomcxplemnotnn0  43419  uzwo4  44043  disjf1o  44190  icof  44218  allbutfiinf  44430  supminfxr  44474  supminfxr2  44479  fsumsupp0  44594  sumnnodd  44646  fnlimabslt  44695  liminfvalxr  44799  ioodvbdlimc1lem1  44947  dvnprodlem1  44962  dvnprodlem2  44963  stoweidlem14  45030  stoweidlem34  45050  stoweidlem44  45060  stoweidlem50  45066  stoweidlem51  45067  stoweidlem52  45068  stoweidlem57  45073  stoweidlem59  45075  fourierdlem19  45142  fourierdlem20  45143  fourierdlem25  45148  fourierdlem31  45154  fourierdlem37  45160  fourierdlem42  45165  fourierdlem51  45173  fourierdlem54  45176  fourierdlem64  45186  fourierdlem79  45201  elaa2lem  45249  etransclem16  45266  etransclem24  45274  etransclem31  45281  etransclem33  45283  etransclem34  45284  etransclem48  45298  salgencl  45348  salexct  45350  salgenuni  45353  subsaliuncllem  45373  meadjiunlem  45481  caragenss  45520  caratheodory  45544  ovnlecvr  45574  ovnlerp  45578  ovn0lem  45581  ovnsubaddlem1  45586  hoidmv1lelem1  45607  hoidmv1lelem3  45609  hoidmvlelem1  45611  hoidmvlelem2  45612  hoidmvlelem3  45613  hoidmvlelem4  45614  ovnhoilem1  45617  ovnhoilem2  45618  ovnlecvr2  45626  ovncvr2  45627  opnvonmbllem2  45649  ovolval4lem1  45665  pimconstlt1  45718  pimiooltgt  45726  pimgtmnf2  45730  pimdecfgtioc  45731  pimincfltioc  45732  pimdecfgtioo  45733  pimincfltioo  45734  sssmf  45754  incsmflem  45757  smfaddlem1  45779  smfaddlem2  45780  decsmflem  45782  smflimlem1  45787  smflimlem2  45788  smflimlem3  45789  smfrec  45805  smfmullem4  45810  smfdiv  45813  smfsuplem1  45827  smfsuplem3  45829  smfinflem  45833  smflimsuplem1  45836  smflimsuplem7  45842  smfliminflem  45846  sprsymrelfolem1  46460  prmdvdsfmtnof1lem1  46552  prmdvdsfmtnof  46554  perfectALTVlem2  46690  oddibas  46851  2zlidl  46922  2zrngbas  46924  2zrng0  46926  isclatd  47697  topclat  47712