Theorem ssrab2 4030

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

Syntax hints:  {crab 3395   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-ss 3919

This theorem is referenced by:  ssrab3  4032  ssrabeq  4034  iinrab2  5018  riinrab  5032  rabelpw  5274  rabexgOLD  5276  frminex  5595  wereu2  5613  predres  6286  frpomin  6287  frpoinsg  6290  ssimaex  6907  f1oresrab  7060  weniso  7288  canth  7300  riotacl  7320  riotassuni  7343  onminesb  7726  onminsb  7727  onintrab  7729  onnminsb  7732  onminex  7735  tfisg  7784  tfis  7785  suppssdm  8107  fnsuppres  8121  oeeulem  8516  nnawordex  8552  pmvalg  8761  fineqvlem  9150  ordtypelem3  9406  ordtypelem4  9407  ordtypelem6  9409  hartogs  9430  card2on  9440  wdom2d  9466  oemapvali  9574  frinsg  9641  tz9.12lem1  9677  tz9.12lem3  9679  rankf  9684  cardf2  9833  cardid2  9843  cardmin2  9889  acni3  9935  dfac2a  10018  cofsmo  10157  coftr  10161  fin2i2  10206  isfin2-2  10207  enfin2i  10209  fin1a2lem11  10298  fin1a2lem12  10299  axdc3lem4  10341  ac6  10368  ondomon  10451  alephval2  10460  pwfseqlem1  10546  pwfseqlem3  10548  wunccl  10632  tskmcl  10729  infm3  12078  uzf  12732  nnwos  12810  supminf  12830  zsupss  12832  rpnnen1lem1  12873  rpnnen1lem3  12874  rpnnen1lem5  12876  ixxf  13252  fzf  13408  flval3  13716  rabssnn0fi  13890  expge0  14002  expge1  14003  hashbclem  14356  01sqrexlem3  15148  rlimrege0  15483  incexc2  15742  bitsf  16335  bitsfzolem  16342  sadadd2lem  16367  sadadd3  16369  sadcl  16370  smupf  16386  smuval2  16390  smupvallem  16391  smucl  16392  smueqlem  16398  lcmcllem  16504  lcmn0cl  16505  lcmledvds  16507  lcmfval  16529  lcmfcllem  16533  lcmfn0cl  16534  lcmfledvds  16540  phicl2  16676  phibnd  16679  hashdvds  16683  phiprmpw  16684  phimullem  16687  eulerth  16691  phisum  16699  odzcllem  16701  odzdvds  16704  prmreclem1  16825  prmreclem2  16826  prmreclem3  16827  prmreclem4  16828  prmreclem5  16829  hashbccl  16912  prmgaplem3  16962  prmgaplem4  16963  prdsds  17365  mrcflem  17509  isacs1i  17560  wunnat  17863  dmcoass  17970  lublecl  18262  lubid  18263  rabsubmgmd  18609  mgmhmeql  18621  issubmd  18711  mhmeql  18731  cntzval  19231  cntzssv  19238  symgsssg  19377  symgfisg  19378  pmtrdifellem4  19389  odfval  19442  odlem1  19445  odlem2  19449  odngen  19487  gexlem1  19489  gexlem2  19492  sylow2alem2  19528  sylow2blem3  19532  oddvdssubg  19765  cyggex2  19807  ablfaclem3  19999  rgspncl  20526  lssacs  20898  lspf  20905  ocvfval  21601  ocvval  21602  dsmmval2  21671  dsmmsubg  21678  asplss  21809  aspsubrg  21811  psrass1lem  21867  psrdi  21900  psrdir  21901  psrass23l  21902  psrass23  21904  resspsrmul  21911  mplbas  21925  mplsubglem  21934  mplsubrglem  21939  mplmonmul  21969  psropprmul  22148  scmatlss  22438  smadiadet  22583  pmatcoe1fsupp  22614  cpmatsubgpmat  22633  fctop  22917  cctop  22919  ppttop  22920  epttop  22922  clscld  22960  neips  23026  neiptopnei  23045  ordtbaslem  23101  ordtuni  23103  ordtcld1  23110  ordtcld2  23111  cnpfval  23147  iscnp2  23152  cmpcov2  23303  cmpsublem  23312  tgcmp  23314  conncompcld  23347  1stcfb  23358  2ndc1stc  23364  2ndcdisj  23369  finlocfin  23433  kgentopon  23451  xkotf  23498  txkgen  23565  xkococnlem  23572  imastopn  23633  kqffn  23638  opnfbas  23755  flimfnfcls  23941  alexsubALT  23964  ptcmplem2  23966  symgtgp  24019  tgpconncompeqg  24025  tgpconncomp  24026  ghmcnp  24028  tsmsfbas  24041  eltsms  24046  utoptop  24147  utopbas  24148  blfvalps  24296  blfps  24319  blf  24320  nmoffn  24624  nmofval  24627  nmogelb  24629  nmolb  24630  nmof  24632  ishtpy  24896  clsocv  25175  rrxnm  25316  rrxbasefi  25335  minveclem3b  25353  minveclem4  25357  ovolcl  25404  ovollb  25405  ovolgelb  25406  ovolge0  25407  ovolshftlem1  25435  ovolshft  25437  ovolscalem1  25439  ovolscalem2  25440  ovolsca  25441  ovolicc2lem3  25445  shftmbl  25464  iundisj  25474  dyadmax  25524  dyadmbllem  25525  opnmbllem  25527  mdegmullem  26008  uc1pval  26070  mon1pval  26072  elqaalem1  26252  elqaalem3  26254  aannenlem2  26262  aalioulem2  26266  radcnvcl  26351  radcnvlt1  26352  radcnvle  26354  ftalem4  27011  ftalem5  27012  efnnfsumcl  27038  isppw  27049  sgmval2  27078  efchtdvds  27094  sqff1o  27117  fsumdvdsdiaglem  27118  fsumdvdsdiag  27119  fsumdvdscom  27120  musum  27126  muinv  27128  sgmmul  27137  ppiub  27140  vmasum  27152  logfac2  27153  perfectlem2  27166  lgsfcl  27241  lgscl  27247  lgsquadlem1  27316  lgsquadlem2  27317  rpvmasumlem  27423  mudivsum  27466  mulogsum  27468  mulog2sumlem2  27471  vmalogdivsum2  27474  logsqvma  27478  logsqvma2  27479  selberglem3  27483  selberg  27484  selberg34r  27507  pntsval2  27512  pntrlog2bndlem1  27513  sltval2  27593  conway  27738  eqscut2  27745  scutun12  27749  scutbdaybnd  27754  scutbdaybnd2  27755  scutbdaylt  27757  bday1s  27773  cuteq0  27774  madef  27795  leftssold  27822  rightssold  27823  madebdaylemlrcut  27842  cofcut1  27862  cofcutr  27866  cutlt  27874  precsexlem8  28150  precsexlem11  28153  onssno  28189  onscutlt  28199  onsiso  28203  bdayon  28207  bdayn0p1  28292  tglnunirn  28524  tglnssp  28528  incistruhgr  29055  upgrss  29064  upgrn0  29065  upgruhgr  29078  usgrss  29150  uspgrushgr  29153  ushgredgedg  29205  ushgredgedgloop  29207  vtxdun  29458  vtxdginducedm1  29520  wlknwwlksnbij  29864  hashwwlksnext  29890  frcond3  30244  numclwlk1lem2  30345  ocsh  31258  spancl  31311  shsval2i  31362  ococin  31383  chsupid  31387  speccl  31874  hatomistici  32337  chpssati  32338  iundisjf  32564  aciunf1  32640  fpwrelmap  32711  iundisjfi  32773  pwrssmgc  32976  cycpmco2f1  33088  cycpmco2rn  33089  cycpmco2lem1  33090  cycpmco2lem2  33091  cycpmco2lem3  33092  cycpmco2lem4  33093  cycpmco2lem5  33094  cycpmco2lem6  33095  cycpmco2lem7  33096  cycpmco2  33097  fxpss  33130  nsgmgclem  33371  mplvrpmlem  33568  mplvrpmga  33570  mplvrpmrhm  33572  esplylem  33582  esplympl  33583  esplymhp  33584  esplyfv1  33585  esplyfv  33586  constrsuc  33746  locfinreflem  33848  zarclsiin  33879  zarcls  33882  zartopn  33883  esumrnmpt2  34076  esumpinfval  34081  sigagensiga  34149  ldgenpisyslem1  34171  ldgenpisys  34174  measvuni  34222  imambfm  34270  dya2iocuni  34291  omscl  34303  oms0  34305  omsmon  34306  omssubadd  34308  carsgcl  34312  oddpwdc  34362  eulerpartlem1  34375  eulerpartlemt  34379  eulerpartgbij  34380  eulerpartlemmf  34383  eulerpartlemgh  34386  eulerpartlemgs2  34388  ballotlem2  34497  ballotlemfc0  34501  ballotlemfcc  34502  ballotlemfmpn  34503  ballotlemiex  34510  ballotlemsup  34513  ballotlem7  34544  ballotth  34546  reprpmtf1o  34634  breprexplema  34638  hgt750lema  34665  bnj110  34865  bnj1204  35019  bnj1311  35031  fnrelpredd  35097  subfacp1lem6  35217  erdszelem2  35224  connpconn  35267  cvmliftmolem2  35314  cvmliftlem15  35330  cvmlift2lem12  35346  snmlff  35361  satfrnmapom  35402  rankeq1o  36204  finminlem  36351  fnessref  36390  neibastop1  36392  neibastop2lem  36393  weiunlem2  36496  weiunse  36501  bj-rabtr  36963  bj-rabtrAUTO  36965  bj-vecssmod  37314  icoreresf  37385  phpreu  37643  fin2so  37646  poimirlem26  37685  poimirlem31  37690  poimirlem32  37691  opnmbllem0  37695  mblfinlem1  37696  mblfinlem2  37697  ismblfin  37700  mbfposadd  37706  cnambfre  37707  cover2  37754  indexa  37772  fdc  37784  sstotbnd2  37813  sstotbnd3  37815  igenidl  38102  prnc  38106  toycom  39011  lkrlss  39133  atlatmstc  39357  atlatle  39358  glbconN  39415  linepsubN  39790  pmapssat  39797  pmaple  39799  pmapsub  39806  paddssat  39852  diass  41080  diaglbN  41093  diaintclN  41096  diassdvaN  41098  docaclN  41162  dibglbN  41204  dibintclN  41205  diclspsn  41232  dihglblem2N  41332  dih1dimatlem  41367  dihglb2  41380  dochval2  41390  dochcl  41391  dochvalr  41395  doch2val2  41402  dochss  41403  dochocss  41404  lclkr  41571  lclkrs  41577  lcdvbase  41631  lcdvbasess  41632  mapdunirnN  41688  aks4d1p4  42111  aks4d1p5  42112  aks4d1p7  42115  aks4d1p8  42119  sticksstones1  42178  aks6d1c6lem2  42203  grpods  42226  unitscyglem1  42227  unitscyglem2  42228  unitscyglem4  42230  mhpind  42626  mhphf  42629  prjcrv0  42665  infdesc  42675  mzpindd  42778  fiphp3d  42851  rencldnfilem  42852  irrapx1  42860  pellexlem3  42863  pellfundre  42913  pellfundge  42914  pellfundlb  42916  pellfundglb  42917  jm2.22  43027  jm2.23  43028  rpnnen3  43064  pwssplit4  43121  pwfi2f1o  43128  hbtlem6  43161  dgraalem  43177  dgraaub  43180  itgocn  43196  onintunirab  43259  nadd2rabord  43417  nadd1rabord  43421  rfovcnvf1od  44036  fsovfd  44044  fsovcnvlem  44045  binomcxplemdvbinom  44385  binomcxplemcvg  44386  binomcxplemnotnn0  44388  uzwo4  45089  disjf1o  45227  icof  45255  allbutfiinf  45457  supminfxr  45501  supminfxr2  45506  fsumsupp0  45617  sumnnodd  45669  fnlimabslt  45716  liminfvalxr  45820  ioodvbdlimc1lem1  45968  dvnprodlem1  45983  dvnprodlem2  45984  stoweidlem14  46051  stoweidlem34  46071  stoweidlem44  46081  stoweidlem50  46087  stoweidlem51  46088  stoweidlem52  46089  stoweidlem57  46094  stoweidlem59  46096  fourierdlem19  46163  fourierdlem20  46164  fourierdlem25  46169  fourierdlem31  46175  fourierdlem37  46181  fourierdlem42  46186  fourierdlem51  46194  fourierdlem54  46197  fourierdlem64  46207  fourierdlem79  46222  elaa2lem  46270  etransclem16  46287  etransclem24  46295  etransclem31  46302  etransclem33  46304  etransclem34  46305  etransclem48  46319  salgencl  46369  salexct  46371  salgenuni  46374  subsaliuncllem  46394  meadjiunlem  46502  caragenss  46541  caratheodory  46565  ovnlecvr  46595  ovnlerp  46599  ovn0lem  46602  ovnsubaddlem1  46607  hoidmv1lelem1  46628  hoidmv1lelem3  46630  hoidmvlelem1  46632  hoidmvlelem2  46633  hoidmvlelem3  46634  hoidmvlelem4  46635  ovnhoilem1  46638  ovnhoilem2  46639  ovnlecvr2  46647  ovncvr2  46648  opnvonmbllem2  46670  ovolval4lem1  46686  pimconstlt1  46739  pimiooltgt  46747  pimgtmnf2  46751  pimdecfgtioc  46752  pimincfltioc  46753  pimdecfgtioo  46754  pimincfltioo  46755  sssmf  46775  incsmflem  46778  smfaddlem1  46800  smfaddlem2  46801  decsmflem  46803  smflimlem1  46808  smflimlem2  46809  smflimlem3  46810  smfrec  46826  smfmullem4  46831  smfdiv  46834  smfsuplem1  46848  smfsuplem3  46850  smfinflem  46854  smflimsuplem1  46857  smflimsuplem7  46863  smfliminflem  46867  sprsymrelfolem1  47522  prmdvdsfmtnof1lem1  47614  prmdvdsfmtnof  47616  perfectALTVlem2  47752  isubgredg  47896  isubgruhgr  47898  isubgrgrim  47959  uhgrimisgrgric  47961  uspgrlimlem1  48018  uspgrlimlem4  48021  uspgrlim  48022  grlimgrtrilem2  48032  oddibas  48203  2zlidl  48270  2zrngbas  48272  2zrng0  48274  isclatd  49013  topclat  49028