Theorem ssrab2 4026

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

This proof depends on syntax axioms:  {crab 3413   ⊆ wss 3914

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-ss 3915

This theorem is used by:  ssrab3  4028  ssrabeq  4030  iinrab2  5028  riinrab  5044  rabelpw  5298  frminex  5630  wereu2  5648  predres  6343  frpomin  6344  frpoinsg  6347  ssimaex  6971  f1oresrab  7129  weniso  7365  canth  7375  riotacl  7395  riotassuni  7418  onminesb  7808  onminsb  7809  onintrab  7811  onnminsb  7814  onminex  7817  tfisg  7866  tfis  7867  suppssdm  8195  fnsuppres  8209  oeeulem  8611  nnawordex  8647  pmvalg  8858  fineqvlem  9258  ordtypelem3  9515  ordtypelem4  9516  ordtypelem6  9518  hartogs  9539  card2on  9549  wdom2d  9575  oemapvali  9686  frinsg  9756  tz9.12lem1  9795  tz9.12lem3  9797  rankf  9803  cardf2  10025  cardid2  10035  cardmin2  10081  acni3  10127  dfac2a  10209  cofsmo  10348  coftr  10352  fin2i2  10397  isfin2-2  10398  enfin2i  10400  fin1a2lem11  10489  fin1a2lem12  10490  axdc3lem4  10532  ac6  10559  ondomon  10648  alephval2  10658  pwfseqlem1  10744  pwfseqlem3  10746  wunccl  10830  tskmcl  10927  infm3  12277  uzf  12969  nnwos  13043  supminf  13063  zsupss  13065  rpnnen1lem1  13107  rpnnen1lem3  13108  rpnnen1lem5  13110  ixxf  13487  fzf  13644  flval3  13956  rabssnn0fi  14130  expge0  14242  expge1  14243  hashbclem  14598  01sqrexlem3  15412  rlimrege0  15747  incexc2  16008  bitsf  16598  bitsfzolem  16605  sadadd2lem  16630  sadadd3  16632  sadcl  16633  smupf  16649  smuval2  16653  smupvallem  16654  smucl  16655  smueqlem  16661  lcmcllem  16772  lcmn0cl  16773  lcmledvds  16775  lcmfval  16797  lcmfcllem  16801  lcmfn0cl  16802  lcmfledvds  16808  phicl2  16946  phibnd  16949  hashdvds  16953  phiprmpw  16954  phimullem  16957  eulerth  16961  phisum  16969  odzcllem  16971  odzdvds  16974  prmreclem1  17095  prmreclem2  17096  prmreclem3  17097  prmreclem4  17098  prmreclem5  17099  hashbccl  17182  prmgaplem3  17232  prmgaplem4  17233  prdsds  17636  mrcflem  17781  isacs1i  17832  wunnat  18135  dmcoass  18242  lublecl  18534  lubid  18535  rabsubmgmd  18894  mgmhmeql  18906  issubmd  19002  mhmeql  19023  cntzval  19536  cntzssv  19543  symgsssg  19682  symgfisg  19683  pmtrdifellem4  19694  odfval  19747  odlem1  19750  odlem2  19754  odngen  19792  gexlem1  19794  gexlem2  19797  sylow2alem2  19833  sylow2blem3  19837  oddvdssubg  20070  cyggex2  20112  ablfaclem3  20304  rgspncl  20866  lssacs  21243  lspf  21250  ocvfval  21973  ocvval  21974  dsmmval2  22043  dsmmsubg  22050  asplss  22182  aspsubrg  22184  psrass1lem  22242  psrdi  22273  psrdir  22274  psrass23l  22275  psrass23  22277  resspsrmul  22284  mplbas  22298  mplsubglem  22307  mplsubrglem  22312  mplmonmul  22346  psropprmul  22556  scmatlss  22841  smadiadet  22986  pmatcoe1fsupp  23020  cpmatsubgpmat  23039  fctop  23323  cctop  23325  ppttop  23326  epttop  23328  clscld  23366  neips  23432  neiptopnei  23451  ordtbaslem  23507  ordtuni  23509  ordtcld1  23516  ordtcld2  23517  cnpfval  23553  iscnp2  23558  cmpcov2  23709  cmpsublem  23718  tgcmp  23720  conncompcld  23753  1stcfb  23764  2ndc1stc  23770  2ndcdisj  23776  finlocfin  23840  kgentopon  23858  xkotf  23905  txkgen  23972  xkococnlem  23979  imastopn  24040  kqffn  24045  opnfbas  24162  flimfnfcls  24348  alexsubALT  24371  ptcmplem2  24373  symgtgp  24426  tgpconncompeqg  24432  tgpconncomp  24433  ghmcnp  24435  tsmsfbas  24448  eltsms  24453  utoptop  24554  utopbas  24555  blfvalps  24703  blfps  24726  blf  24727  nmoffn  25031  nmofval  25034  nmogelb  25036  nmolb  25037  nmof  25039  ishtpy  25294  clsocv  25572  rrxnm  25713  rrxbasefi  25732  minveclem3b  25750  minveclem4  25754  ovolcl  25800  ovollb  25801  ovolgelb  25802  ovolge0  25803  ovolshftlem1  25831  ovolshft  25833  ovolscalem1  25835  ovolscalem2  25836  ovolsca  25837  ovolicc2lem3  25841  shftmbl  25860  iundisj  25870  dyadmax  25920  dyadmbllem  25921  opnmbllem  25923  mdegmullem  26397  uc1pval  26459  mon1pval  26461  elqaalem1  26643  elqaalem3  26645  aannenlem2  26657  aalioulem2  26661  radcnvcl  26745  radcnvlt1  26746  radcnvle  26748  ftalem4  27404  ftalem5  27405  efnnfsumcl  27431  isppw  27442  sgmval2  27471  efchtdvds  27487  sqff1o  27510  fsumdvdsdiaglem  27511  fsumdvdsdiag  27512  fsumdvdscom  27513  musum  27519  muinv  27521  sgmmul  27529  ppiub  27532  vmasum  27544  logfac2  27545  perfectlem2  27558  lgsfcl  27633  lgscl  27639  lgsquadlem1  27708  lgsquadlem2  27709  rpvmasumlem  27815  mudivsum  27858  mulogsum  27860  mulog2sumlem2  27863  vmalogdivsum2  27866  logsqvma  27870  logsqvma2  27871  selberglem3  27875  selberg  27876  selberg34r  27899  pntsval2  27904  pntrlog2bndlem1  27905  infdesc  27968  ltsval2  28014  conway  28166  eqcuts2  28173  cutsun12  28177  cutbdaybnd  28182  cutbdaybnd2  28183  cutbdaylt  28185  bday1  28201  cuteq0  28202  madef  28223  leftssold  28258  rightssold  28259  madebdaylemlrcut  28286  sltsbday  28304  cofcut1  28307  cofcutr  28311  cutlt  28319  precsexlem8  28601  precsexlem11  28604  onssno  28641  oncutlt  28651  oniso  28658  bdayons  28663  bdayn0p1  28756  tglnunirn  29012  tglnssp  29016  plngrnssp  29258  plngssp  29260  incistruhgr  29658  upgrss  29667  upgrn0  29668  upgruhgr  29681  usgrss  29756  uspgrushgr  29759  ushgredgedg  29811  ushgredgedgloop  29813  vtxdun  30063  vtxdginducedm1  30125  wlknwwlksnbij  30478  hashwwlksnext  30504  frcond3  30871  numclwlk1lem2  30972  ocsh  31886  spancl  31939  shsval2i  31990  ococin  32011  chsupid  32015  speccl  32502  hatomistici  32965  chpssati  32966  iundisjf  33184  aciunf1  33258  fpwrelmap  33326  iundisjfi  33389  pwrssmgc  33562  cycpmco2f1  33686  cycpmco2rn  33687  cycpmco2lem1  33688  cycpmco2lem2  33689  cycpmco2lem3  33690  cycpmco2lem4  33691  cycpmco2lem5  33692  cycpmco2lem6  33693  cycpmco2lem7  33694  cycpmco2  33695  fxpss  33728  nsgmgclem  33963  0mplrim  34147  selvply1rhmlemb  34152  selvply1rhm0  34159  extvfvcl  34169  mplmulmvr  34172  evlextv  34175  mplvrpmlem  34176  mplvrpmga  34178  mplvrpmrhm  34180  psrmonmul  34183  esplylem  34199  esplympl  34200  esplymhp  34201  esplyfv1  34202  esplyfv  34203  esplyfval3  34205  esplyfval1  34206  esplyfvaln  34207  constrsuc  34371  locfinreflem  34473  zarclsiin  34504  zarcls  34507  zartopn  34508  esumrnmpt2  34701  esumpinfval  34706  sigagensiga  34775  ldgenpisyslem1  34797  ldgenpisys  34800  measvuni  34848  imambfm  34895  dya2iocuni  34916  omscl  34928  oms0  34930  omsmon  34931  omssubadd  34933  carsgcl  34937  oddpwdc  34987  eulerpartlem1  35000  eulerpartlemt  35004  eulerpartgbij  35005  eulerpartlemmf  35008  eulerpartlemgh  35011  eulerpartlemgs2  35013  ballotlem2  35122  ballotlemfc0  35126  ballotlemfcc  35127  ballotlemfmpn  35128  ballotlemiex  35135  ballotlemsup  35138  ballotlem7  35169  ballotth  35171  reprpmtf1o  35256  breprexplema  35260  hgt750lema  35287  bnj110  35489  bnj1204  35643  bnj1311  35655  fnrelpredd  35721  subfacp1lem6  35951  erdszelem2  35958  connpconn  36001  cvmliftmolem2  36048  cvmliftlem15  36064  cvmlift2lem12  36080  snmlff  36095  satfrnmapom  36136  rankeq1o  36933  nmuladdel  36962  finminlem  37107  fnessref  37146  neibastop1  37148  neibastop2lem  37149  weiunlem  37252  weiunse  37257  bj-rabtr  37844  bj-rabtrAUTO  37846  bj-vecssmod  38204  icoreresf  38277  phpreu  38529  fin2so  38532  poimirlem26  38566  poimirlem31  38571  poimirlem32  38572  opnmbllem0  38576  mblfinlem1  38577  mblfinlem2  38578  ismblfin  38581  mbfposadd  38587  cnambfre  38588  cover2  38651  indexa  38669  fdc  38681  sstotbnd2  38710  sstotbnd3  38712  igenidl  38999  prnc  39003  toycom  40032  lkrlss  40154  atlatmstc  40378  atlatle  40379  glbconN  40436  linepsubN  40811  pmapssat  40818  pmaple  40820  pmapsub  40827  paddssat  40873  diass  42101  diaglbN  42114  diaintclN  42117  diassdvaN  42119  docaclN  42183  dibglbN  42225  dibintclN  42226  diclspsn  42253  dihglblem2N  42353  dih1dimatlem  42388  dihglb2  42401  dochval2  42411  dochcl  42412  dochvalr  42416  doch2val2  42423  dochss  42424  dochocss  42425  lclkr  42592  lclkrs  42598  lcdvbase  42652  lcdvbasess  42653  mapdunirnN  42709  aks4d1p4  43131  aks4d1p5  43132  aks4d1p7  43135  aks4d1p8  43139  sticksstones1  43198  aks6d1c6lem2  43223  grpods  43246  unitscyglem1  43247  unitscyglem2  43248  unitscyglem4  43250  mhpind  43624  mhphf  43627  frlmnzcoordinf  43656  frlmnzcoordcl  43657  frlmnzcoordn0  43659  prjcrv0  43671  mzpindd  43758  fiphp3d  43827  rencldnfilem  43828  irrapx1  43836  pellexlem3  43839  pellfundre  43889  pellfundge  43890  pellfundlb  43892  pellfundglb  43893  jm2.22  44003  jm2.23  44004  rpnnen3  44040  pwssplit4  44092  pwfi2f1o  44099  hbtlem6  44132  dgraalem  44148  dgraaub  44151  itgocn  44167  onintunirab  44230  nadd2rabord  44388  nadd1rabord  44392  rfovcnvf1od  45005  fsovfd  45013  fsovcnvlem  45014  binomcxplemdvbinom  45338  binomcxplemcvg  45339  binomcxplemnotnn0  45341  uzwo4  46071  disjf1o  46207  icof  46233  allbutfiinf  46431  supminfxr  46475  supminfxr2  46480  fsumsupp0  46591  sumnnodd  46643  fnlimabslt  46690  liminfvalxr  46794  ioodvbdlimc1lem1  46942  dvnprodlem1  46957  dvnprodlem2  46958  stoweidlem14  47025  stoweidlem34  47045  stoweidlem44  47055  stoweidlem50  47061  stoweidlem51  47062  stoweidlem52  47063  stoweidlem57  47068  stoweidlem59  47070  fourierdlem19  47137  fourierdlem20  47138  fourierdlem25  47143  fourierdlem31  47149  fourierdlem37  47155  fourierdlem42  47160  fourierdlem51  47168  fourierdlem54  47171  fourierdlem64  47181  fourierdlem79  47196  elaa2lem  47244  etransclem16  47261  etransclem24  47269  etransclem31  47276  etransclem33  47278  etransclem34  47279  etransclem48  47293  salgencl  47343  salexct  47345  salgenuni  47348  subsaliuncllem  47368  meadjiunlem  47476  caragenss  47515  caratheodory  47539  ovnlecvr  47569  ovnlerp  47573  ovn0lem  47576  ovnsubaddlem1  47581  hoidmv1lelem1  47602  hoidmv1lelem3  47604  hoidmvlelem1  47606  hoidmvlelem2  47607  hoidmvlelem3  47608  hoidmvlelem4  47609  ovnhoilem1  47612  ovnhoilem2  47613  ovnlecvr2  47621  ovncvr2  47622  opnvonmbllem2  47644  ovolval4lem1  47660  pimconstlt1  47713  pimgtmnf2  47725  pimdecfgtioc  47726  pimincfltioc  47727  pimdecfgtioo  47728  pimincfltioo  47729  sssmf  47749  incsmflem  47752  smfaddlem1  47774  smfaddlem2  47775  decsmflem  47777  smflimlem1  47782  smflimlem2  47783  smflimlem3  47784  smfrec  47800  smfmullem4  47805  smfdiv  47808  smfpimcclem  47818  smfsuplem1  47822  smfsuplem3  47824  smfinflem  47828  smflimsuplem1  47831  smflimsuplem7  47837  smfliminflem  47841  tmachlem-agreeself  47947  tmachlem-agreeprod  47948  tmachlem-uassst  47954  tmachlem-extpcover  47956  tmachlem-agreefin  47959  sprsymrelfolem1  48575  prmdvdsfmtnof1lem1  48670  prmdvdsfmtnof  48672  perfectALTVlem2  48821  isubgredg  48965  isubgruhgr  48967  isubgrgrim  49028  uhgrimisgrgric  49030  uspgrlimlem1  49087  uspgrlimlem4  49090  uspgrlim  49091  grlimgrtrilem2  49101  oddibas  49271  2zlidl  49338  2zrngbas  49340  2zrng0  49342  isclatd  50092  topclat  50107  dvsec  50857  dvcsc  50858  dvcot  50859