Theorem ssrab2 4005

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

This proof depends on syntax axioms:  {crab 3412   ⊆ wss 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-ss 3896

This theorem is used by:  ssrab3  4007  ssrabeq  4009  iinrab2  5027  riinrab  5043  rabelpw  5297  frminex  5629  wereu2  5647  predres  6342  frpomin  6343  frpoinsg  6346  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  8198  fnsuppres  8212  oeeulem  8614  nnawordex  8650  pmvalg  8861  fineqvlem  9261  ordtypelem3  9518  ordtypelem4  9519  ordtypelem6  9521  hartogs  9542  card2on  9552  wdom2d  9578  oemapvali  9689  frinsg  9759  tz9.12lem1  9798  tz9.12lem3  9800  rankf  9806  cardf2  10028  cardid2  10038  cardmin2  10084  acni3  10130  dfac2a  10212  cofsmo  10351  coftr  10355  fin2i2  10400  isfin2-2  10401  enfin2i  10403  fin1a2lem11  10492  fin1a2lem12  10493  axdc3lem4  10535  ac6  10562  ondomon  10651  alephval2  10661  pwfseqlem1  10747  pwfseqlem3  10749  wunccl  10833  tskmcl  10930  infm3  12280  uzf  12972  nnwos  13046  supminf  13066  zsupss  13068  rpnnen1lem1  13110  rpnnen1lem3  13111  rpnnen1lem5  13113  ixxf  13490  fzf  13647  flval3  13959  rabssnn0fi  14133  expge0  14245  expge1  14246  hashbclem  14601  01sqrexlem3  15417  rlimrege0  15752  incexc2  16013  bitsf  16603  bitsfzolem  16610  sadadd2lem  16635  sadadd3  16637  sadcl  16638  smupf  16654  smuval2  16658  smupvallem  16659  smucl  16660  smueqlem  16666  lcmcllem  16777  lcmn0cl  16778  lcmledvds  16780  lcmfval  16802  lcmfcllem  16806  lcmfn0cl  16807  lcmfledvds  16813  phicl2  16951  phibnd  16954  hashdvds  16958  phiprmpw  16959  phimullem  16962  eulerth  16966  phisum  16974  odzcllem  16976  odzdvds  16979  prmreclem1  17100  prmreclem3  17102  prmreclem4  17103  prmreclem5  17104  hashbccl  17187  prmgaplem3  17237  prmgaplem4  17238  prdsds  17641  mrcflem  17786  isacs1i  17837  wunnat  18140  dmcoass  18247  lublecl  18539  lubid  18540  rabsubmgmd  18899  mgmhmeql  18911  issubmd  19007  mhmeql  19028  cntzval  19541  cntzssv  19548  symgsssg  19687  symgfisg  19688  pmtrdifellem4  19699  odfval  19752  odlem1  19755  odlem2  19759  odngen  19797  gexlem1  19799  gexlem2  19802  sylow2alem2  19838  sylow2blem3  19842  oddvdssubg  20075  cyggex2  20117  ablfaclem3  20309  rgspncl  20871  lssacs  21248  lspf  21255  ocvfval  21978  ocvval  21979  dsmmval2  22048  dsmmsubg  22055  asplss  22187  aspsubrg  22189  psrass1lem  22247  psrdi  22278  psrdir  22279  psrass23l  22280  psrass23  22282  resspsrmul  22289  mplbas  22303  mplsubglem  22312  mplsubrglem  22317  mplmonmul  22351  psropprmul  22561  scmatlss  22846  smadiadet  22991  pmatcoe1fsupp  23025  cpmatsubgpmat  23044  fctop  23328  cctop  23330  ppttop  23331  epttop  23333  clscld  23371  neips  23437  neiptopnei  23456  ordtbaslem  23512  ordtuni  23514  ordtcld1  23521  ordtcld2  23522  cnpfval  23558  iscnp2  23563  cmpcov2  23714  cmpsublem  23723  tgcmp  23725  conncompcld  23758  1stcfb  23769  2ndc1stc  23775  2ndcdisj  23781  finlocfin  23845  kgentopon  23863  xkotf  23910  txkgen  23977  xkococnlem  23984  imastopn  24045  kqffn  24050  opnfbas  24167  flimfnfcls  24353  alexsubALT  24376  ptcmplem2  24378  symgtgp  24431  tgpconncompeqg  24437  tgpconncomp  24438  ghmcnp  24440  tsmsfbas  24453  eltsms  24458  utoptop  24559  utopbas  24560  blfvalps  24708  blfps  24731  blf  24732  nmoffn  25036  nmofval  25039  nmogelb  25041  nmolb  25042  nmof  25044  ishtpy  25299  clsocv  25577  rrxnm  25718  rrxbasefi  25737  minveclem3b  25755  minveclem4  25759  ovolcl  25805  ovollb  25806  ovolgelb  25807  ovolge0  25808  ovolshftlem1  25836  ovolshft  25838  ovolscalem1  25840  ovolscalem2  25841  ovolsca  25842  ovolicc2lem3  25846  shftmbl  25865  iundisj  25875  dyadmax  25925  dyadmbllem  25926  opnmbllem  25928  mdegmullem  26402  uc1pval  26464  mon1pval  26466  elqaalem1  26648  elqaalem3  26650  aannenlem2  26662  aalioulem2  26666  radcnvcl  26750  radcnvlt1  26751  radcnvle  26753  ftalem4  27409  ftalem5  27410  efnnfsumcl  27436  isppw  27447  sgmval2  27476  efchtdvds  27492  sqff1o  27515  fsumdvdsdiaglem  27516  fsumdvdsdiag  27517  fsumdvdscom  27518  musum  27524  muinv  27526  sgmmul  27534  ppiub  27537  vmasum  27549  logfac2  27550  perfectlem2  27563  lgsfcl  27638  lgscl  27644  lgsquadlem1  27713  lgsquadlem2  27714  rpvmasumlem  27820  mudivsum  27863  mulogsum  27865  mulog2sumlem2  27868  vmalogdivsum2  27871  logsqvma  27875  logsqvma2  27876  selberglem3  27880  selberg  27881  selberg34r  27904  pntsval2  27909  pntrlog2bndlem1  27910  infdesc  27973  ltsval2  28019  conway  28171  eqcuts2  28178  cutsun12  28182  cutbdaybnd  28187  cutbdaybnd2  28188  cutbdaylt  28190  bday1  28206  cuteq0  28207  madef  28228  leftssold  28263  rightssold  28264  madebdaylemlrcut  28291  sltsbday  28309  cofcut1  28312  cofcutr  28316  cutlt  28324  precsexlem8  28606  precsexlem11  28609  onssno  28646  oncutlt  28656  oniso  28663  bdayons  28668  bdayn0p1  28761  tglnunirn  29017  tglnssp  29021  plngrnssp  29263  plngssp  29265  incistruhgr  29663  upgrss  29672  upgrn0  29673  upgruhgr  29686  usgrss  29761  uspgrushgr  29764  ushgredgedg  29816  ushgredgedgloop  29818  vtxdun  30068  vtxdginducedm1  30130  wlknwwlksnbij  30483  hashwwlksnext  30509  frcond3  30876  numclwlk1lem2  30977  ocsh  31891  spancl  31944  shsval2i  31995  ococin  32016  chsupid  32020  speccl  32507  hatomistici  32970  chpssati  32971  iundisjf  33231  aciunf1  33305  fpwrelmap  33372  iundisjfi  33435  pwrssmgc  33608  cycpmco2f1  33732  cycpmco2rn  33733  cycpmco2lem1  33734  cycpmco2lem2  33735  cycpmco2lem3  33736  cycpmco2lem4  33737  cycpmco2lem5  33738  cycpmco2lem6  33739  cycpmco2lem7  33740  cycpmco2  33741  fxpss  33774  nsgmgclem  34009  0mplrim  34193  selvply1rhmlemb  34198  selvply1rhm0  34205  extvfvcl  34215  mplmulmvr  34218  evlextv  34221  mplvrpmlem  34222  mplvrpmga  34224  mplvrpmrhm  34226  psrmonmul  34229  esplylem  34245  esplympl  34246  esplymhp  34247  esplyfv1  34248  esplyfv  34249  esplyfval3  34251  esplyfval1  34252  esplyfvaln  34253  constrsuc  34417  locfinreflem  34519  zarclsiin  34550  zarcls  34553  zartopn  34554  esumrnmpt2  34747  esumpinfval  34752  sigagensiga  34821  ldgenpisyslem1  34843  ldgenpisys  34846  measvuni  34894  imambfm  34941  dya2iocuni  34962  omscl  34974  oms0  34976  omsmon  34977  omssubadd  34979  carsgcl  34983  oddpwdc  35033  eulerpartlem1  35046  eulerpartlemt  35050  eulerpartgbij  35051  eulerpartlemmf  35054  eulerpartlemgh  35057  eulerpartlemgs2  35059  ballotlem2  35168  ballotlemfc0  35172  ballotlemfcc  35173  ballotlemfmpn  35174  ballotlemiex  35181  ballotlemsup  35184  ballotlem7  35215  ballotth  35217  reprpmtf1o  35302  breprexplema  35306  hgt750lema  35333  bnj110  35535  bnj1204  35689  bnj1311  35701  fnrelpredd  35773  subfacp1lem6  36037  erdszelem2  36044  connpconn  36087  cvmliftmolem2  36134  cvmliftlem15  36150  cvmlift2lem12  36166  snmlff  36181  satfrnmapom  36222  rankeq1o  37025  nmuladdel  37054  finminlem  37199  fnessref  37238  neibastop1  37240  neibastop2lem  37241  weiunlem  37344  weiunse  37349  bj-rabtr  37936  bj-rabtrAUTO  37938  bj-vecssmod  38296  icoreresf  38369  phpreu  38621  fin2so  38624  poimirlem26  38658  poimirlem31  38663  poimirlem32  38664  opnmbllem0  38668  mblfinlem1  38669  mblfinlem2  38670  ismblfin  38673  mbfposadd  38679  cnambfre  38680  cover2  38743  indexa  38761  fdc  38773  sstotbnd2  38802  sstotbnd3  38804  igenidl  39091  prnc  39095  toycom  40124  lkrlss  40246  atlatmstc  40470  atlatle  40471  glbconN  40528  linepsubN  40903  pmapssat  40910  pmaple  40912  pmapsub  40919  paddssat  40965  diass  42193  diaglbN  42206  diaintclN  42209  diassdvaN  42211  docaclN  42275  dibglbN  42317  dibintclN  42318  diclspsn  42345  dihglblem2N  42445  dih1dimatlem  42480  dihglb2  42493  dochval2  42503  dochcl  42504  dochvalr  42508  doch2val2  42515  dochss  42516  dochocss  42517  lclkr  42684  lclkrs  42690  lcdvbase  42744  lcdvbasess  42745  mapdunirnN  42801  aks4d1p4  43223  aks4d1p5  43224  aks4d1p7  43227  aks4d1p8  43231  sticksstones1  43290  aks6d1c6lem2  43315  grpods  43338  unitscyglem1  43339  unitscyglem2  43340  unitscyglem4  43342  mhpind  43716  mhphf  43719  frlmnzcoordinf  43748  frlmnzcoordcl  43749  frlmnzcoordn0  43751  prjcrv0  43763  mzpindd  43851  fiphp3d  43920  rencldnfilem  43921  irrapx1  43929  pellexlem3  43932  pellfundre  43982  pellfundge  43983  pellfundlb  43985  pellfundglb  43986  jm2.22  44096  jm2.23  44097  rpnnen3  44133  pwssplit4  44185  pwfi2f1o  44192  hbtlem6  44225  dgraalem  44241  dgraaub  44244  itgocn  44260  onintunirab  44323  nadd2rabord  44481  nadd1rabord  44485  rfovcnvf1od  45098  fsovfd  45106  fsovcnvlem  45107  binomcxplemdvbinom  45431  binomcxplemcvg  45432  binomcxplemnotnn0  45434  uzwo4  46164  disjf1o  46300  icof  46326  allbutfiinf  46524  supminfxr  46568  supminfxr2  46573  fsumsupp0  46684  sumnnodd  46736  fnlimabslt  46783  liminfvalxr  46887  ioodvbdlimc1lem1  47035  dvnprodlem1  47050  dvnprodlem2  47051  stoweidlem14  47118  stoweidlem34  47138  stoweidlem44  47148  stoweidlem50  47154  stoweidlem51  47155  stoweidlem52  47156  stoweidlem57  47161  stoweidlem59  47163  fourierdlem19  47230  fourierdlem20  47231  fourierdlem25  47236  fourierdlem31  47242  fourierdlem37  47248  fourierdlem42  47253  fourierdlem51  47261  fourierdlem54  47264  fourierdlem64  47274  fourierdlem79  47289  elaa2lem  47337  etransclem16  47354  etransclem24  47362  etransclem31  47369  etransclem33  47371  etransclem34  47372  etransclem48  47386  salgencl  47436  salexct  47438  salgenuni  47441  subsaliuncllem  47461  meadjiunlem  47569  caragenss  47608  caratheodory  47632  ovnlecvr  47662  ovnlerp  47666  ovn0lem  47669  ovnsubaddlem1  47674  hoidmv1lelem1  47695  hoidmv1lelem3  47697  hoidmvlelem1  47699  hoidmvlelem2  47700  hoidmvlelem3  47701  hoidmvlelem4  47702  ovnhoilem1  47705  ovnhoilem2  47706  ovnlecvr2  47714  ovncvr2  47715  opnvonmbllem2  47737  ovolval4lem1  47753  pimconstlt1  47806  pimgtmnf2  47818  pimdecfgtioc  47819  pimincfltioc  47820  pimdecfgtioo  47821  pimincfltioo  47822  sssmf  47842  incsmflem  47845  smfaddlem1  47867  smfaddlem2  47868  decsmflem  47870  smflimlem1  47875  smflimlem2  47876  smflimlem3  47877  smfrec  47893  smfmullem4  47898  smfdiv  47901  smfpimcclem  47911  smfsuplem1  47915  smfsuplem3  47917  smfinflem  47921  smflimsuplem1  47924  smflimsuplem7  47930  smfliminflem  47934  tmachlem-agreeself  48040  tmachlem-agreeprod  48041  tmachlem-uassst  48047  tmachlem-extpcover  48049  tmachlem-agreefin  48052  sprsymrelfolem1  48668  prmdvdsfmtnof1lem1  48763  prmdvdsfmtnof  48765  perfectALTVlem2  48914  isubgredg  49058  isubgruhgr  49060  isubgrgrim  49121  uhgrimisgrgric  49123  uspgrlimlem1  49180  uspgrlimlem4  49183  uspgrlim  49184  grlimgrtrilem2  49194  oddibas  49364  2zlidl  49431  2zrngbas  49433  2zrng0  49435  isclatd  50191  topclat  50206  dvsec  51025  dvcsc  51026  dvcot  51027