Theorem ssrab2 4036

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

Syntax hints:  {crab 3417   ⊆ wss 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-ss 3924

This theorem is referenced by:  ssrab3  4038  ssrabeq  4040  iinrab2  5030  riinrab  5046  rabelpw  5297  rabexgOLD  5299  frminex  5631  wereu2  5649  predres  6330  frpomin  6331  frpoinsg  6334  ssimaex  6956  f1oresrab  7113  weniso  7342  canth  7354  riotacl  7374  riotassuni  7397  onminesb  7780  onminsb  7781  onintrab  7783  onnminsb  7786  onminex  7789  tfisg  7838  tfis  7839  suppssdm  8161  fnsuppres  8175  oeeulem  8575  nnawordex  8611  pmvalg  8822  fineqvlem  9214  ordtypelem3  9470  ordtypelem4  9471  ordtypelem6  9473  hartogs  9494  card2on  9504  wdom2d  9530  oemapvali  9641  frinsg  9711  tz9.12lem1  9747  tz9.12lem3  9749  rankf  9754  cardf2  9917  cardid2  9927  cardmin2  9973  acni3  10019  dfac2a  10101  cofsmo  10241  coftr  10245  fin2i2  10290  isfin2-2  10291  enfin2i  10293  fin1a2lem11  10382  fin1a2lem12  10383  axdc3lem4  10425  ac6  10452  ondomon  10535  alephval2  10545  pwfseqlem1  10631  pwfseqlem3  10633  wunccl  10717  tskmcl  10814  infm3  12165  uzf  12856  nnwos  12930  supminf  12950  zsupss  12952  rpnnen1lem1  12993  rpnnen1lem3  12994  rpnnen1lem5  12996  ixxf  13373  fzf  13530  flval3  13839  rabssnn0fi  14013  expge0  14125  expge1  14126  hashbclem  14479  01sqrexlem3  15285  rlimrege0  15620  incexc2  15882  bitsf  16475  bitsfzolem  16482  sadadd2lem  16507  sadadd3  16509  sadcl  16510  smupf  16526  smuval2  16530  smupvallem  16531  smucl  16532  smueqlem  16538  lcmcllem  16644  lcmn0cl  16645  lcmledvds  16647  lcmfval  16669  lcmfcllem  16673  lcmfn0cl  16674  lcmfledvds  16680  phicl2  16817  phibnd  16820  hashdvds  16824  phiprmpw  16825  phimullem  16828  eulerth  16832  phisum  16840  odzcllem  16842  odzdvds  16845  prmreclem1  16966  prmreclem2  16967  prmreclem3  16968  prmreclem4  16969  prmreclem5  16970  hashbccl  17053  prmgaplem3  17103  prmgaplem4  17104  prdsds  17507  mrcflem  17652  isacs1i  17703  wunnat  18006  dmcoass  18113  lublecl  18405  lubid  18406  rabsubmgmd  18752  mgmhmeql  18764  issubmd  18854  mhmeql  18875  cntzval  19382  cntzssv  19389  symgsssg  19528  symgfisg  19529  pmtrdifellem4  19540  odfval  19593  odlem1  19596  odlem2  19600  odngen  19638  gexlem1  19640  gexlem2  19643  sylow2alem2  19679  sylow2blem3  19683  oddvdssubg  19916  cyggex2  19958  ablfaclem3  20150  rgspncl  20689  lssacs  21057  lspf  21064  ocvfval  21776  ocvval  21777  dsmmval2  21846  dsmmsubg  21853  asplss  21983  aspsubrg  21985  psrass1lem  22043  psrdi  22074  psrdir  22075  psrass23l  22076  psrass23  22078  resspsrmul  22085  mplbas  22099  mplsubglem  22108  mplsubrglem  22113  mplmonmul  22147  psropprmul  22357  scmatlss  22643  smadiadet  22788  pmatcoe1fsupp  22819  cpmatsubgpmat  22838  fctop  23122  cctop  23124  ppttop  23125  epttop  23127  clscld  23165  neips  23231  neiptopnei  23250  ordtbaslem  23306  ordtuni  23308  ordtcld1  23315  ordtcld2  23316  cnpfval  23352  iscnp2  23357  cmpcov2  23508  cmpsublem  23517  tgcmp  23519  conncompcld  23552  1stcfb  23563  2ndc1stc  23569  2ndcdisj  23574  finlocfin  23638  kgentopon  23656  xkotf  23703  txkgen  23770  xkococnlem  23777  imastopn  23838  kqffn  23843  opnfbas  23960  flimfnfcls  24146  alexsubALT  24169  ptcmplem2  24171  symgtgp  24224  tgpconncompeqg  24230  tgpconncomp  24231  ghmcnp  24233  tsmsfbas  24246  eltsms  24251  utoptop  24352  utopbas  24353  blfvalps  24501  blfps  24524  blf  24525  nmoffn  24829  nmofval  24832  nmogelb  24834  nmolb  24835  nmof  24837  ishtpy  25092  clsocv  25370  rrxnm  25511  rrxbasefi  25530  minveclem3b  25548  minveclem4  25552  ovolcl  25598  ovollb  25599  ovolgelb  25600  ovolge0  25601  ovolshftlem1  25629  ovolshft  25631  ovolscalem1  25633  ovolscalem2  25634  ovolsca  25635  ovolicc2lem3  25639  shftmbl  25658  iundisj  25668  dyadmax  25718  dyadmbllem  25719  opnmbllem  25721  mdegmullem  26196  uc1pval  26258  mon1pval  26260  elqaalem1  26441  elqaalem3  26443  aannenlem2  26451  aalioulem2  26455  radcnvcl  26538  radcnvlt1  26539  radcnvle  26541  ftalem4  27198  ftalem5  27199  efnnfsumcl  27225  isppw  27236  sgmval2  27265  efchtdvds  27281  sqff1o  27304  fsumdvdsdiaglem  27305  fsumdvdsdiag  27306  fsumdvdscom  27307  musum  27313  muinv  27315  sgmmul  27323  ppiub  27326  vmasum  27338  logfac2  27339  perfectlem2  27352  lgsfcl  27427  lgscl  27433  lgsquadlem1  27502  lgsquadlem2  27503  rpvmasumlem  27609  mudivsum  27652  mulogsum  27654  mulog2sumlem2  27657  vmalogdivsum2  27660  logsqvma  27664  logsqvma2  27665  selberglem3  27669  selberg  27670  selberg34r  27693  pntsval2  27698  pntrlog2bndlem1  27699  ltsval2  27778  conway  27930  eqcuts2  27937  cutsun12  27941  cutbdaybnd  27946  cutbdaybnd2  27947  cutbdaylt  27949  bday1  27965  cuteq0  27966  madef  27987  leftssold  28022  rightssold  28023  madebdaylemlrcut  28050  sltsbday  28068  cofcut1  28071  cofcutr  28075  cutlt  28083  precsexlem8  28365  precsexlem11  28368  onssno  28405  oncutlt  28415  oniso  28422  bdayons  28427  bdayn0p1  28520  tglnunirn  28775  tglnssp  28779  plngrnssp  29009  plngssp  29011  incistruhgr  29338  upgrss  29347  upgrn0  29348  upgruhgr  29361  usgrss  29433  uspgrushgr  29436  ushgredgedg  29488  ushgredgedgloop  29490  vtxdun  29740  vtxdginducedm1  29802  wlknwwlksnbij  30146  hashwwlksnext  30172  frcond3  30529  numclwlk1lem2  30630  ocsh  31544  spancl  31597  shsval2i  31648  ococin  31669  chsupid  31673  speccl  32160  hatomistici  32623  chpssati  32624  iundisjf  32844  aciunf1  32920  fpwrelmap  32990  iundisjfi  33053  pwrssmgc  33233  cycpmco2f1  33357  cycpmco2rn  33358  cycpmco2lem1  33359  cycpmco2lem2  33360  cycpmco2lem3  33361  cycpmco2lem4  33362  cycpmco2lem5  33363  cycpmco2lem6  33364  cycpmco2lem7  33365  cycpmco2  33366  fxpss  33399  nsgmgclem  33636  0mplrim  33821  selvply1rhmlemb  33826  selvply1rhm0  33833  extvfvcl  33843  mplmulmvr  33846  evlextv  33849  mplvrpmlem  33850  mplvrpmga  33852  mplvrpmrhm  33854  psrmonmul  33857  esplylem  33873  esplympl  33874  esplymhp  33875  esplyfv1  33876  esplyfv  33877  esplyfval3  33879  esplyfval1  33880  esplyfvaln  33881  constrsuc  34045  locfinreflem  34147  zarclsiin  34178  zarcls  34181  zartopn  34182  esumrnmpt2  34375  esumpinfval  34380  sigagensiga  34448  ldgenpisyslem1  34470  ldgenpisys  34473  measvuni  34521  imambfm  34569  dya2iocuni  34590  omscl  34602  oms0  34604  omsmon  34605  omssubadd  34607  carsgcl  34611  oddpwdc  34661  eulerpartlem1  34674  eulerpartlemt  34678  eulerpartgbij  34679  eulerpartlemmf  34682  eulerpartlemgh  34685  eulerpartlemgs2  34687  ballotlem2  34796  ballotlemfc0  34800  ballotlemfcc  34801  ballotlemfmpn  34802  ballotlemiex  34809  ballotlemsup  34812  ballotlem7  34843  ballotth  34845  reprpmtf1o  34930  breprexplema  34934  hgt750lema  34961  bnj110  35163  bnj1204  35317  bnj1311  35329  fnrelpredd  35397  subfacp1lem6  35548  erdszelem2  35555  connpconn  35598  cvmliftmolem2  35645  cvmliftlem15  35661  cvmlift2lem12  35677  snmlff  35692  satfrnmapom  35733  rankeq1o  36534  finminlem  36691  fnessref  36730  neibastop1  36732  neibastop2lem  36733  weiunlem  36836  weiunse  36841  bj-rabtr  37427  bj-rabtrAUTO  37429  bj-vecssmod  37785  icoreresf  37858  phpreu  38115  fin2so  38118  poimirlem26  38157  poimirlem31  38162  poimirlem32  38163  opnmbllem0  38167  mblfinlem1  38168  mblfinlem2  38169  ismblfin  38172  mbfposadd  38178  cnambfre  38179  cover2  38226  indexa  38244  fdc  38256  sstotbnd2  38285  sstotbnd3  38287  igenidl  38574  prnc  38578  toycom  39609  lkrlss  39731  atlatmstc  39955  atlatle  39956  glbconN  40013  linepsubN  40388  pmapssat  40395  pmaple  40397  pmapsub  40404  paddssat  40450  diass  41678  diaglbN  41691  diaintclN  41694  diassdvaN  41696  docaclN  41760  dibglbN  41802  dibintclN  41803  diclspsn  41830  dihglblem2N  41930  dih1dimatlem  41965  dihglb2  41978  dochval2  41988  dochcl  41989  dochvalr  41993  doch2val2  42000  dochss  42001  dochocss  42002  lclkr  42169  lclkrs  42175  lcdvbase  42229  lcdvbasess  42230  mapdunirnN  42286  aks4d1p4  42708  aks4d1p5  42709  aks4d1p7  42712  aks4d1p8  42716  sticksstones1  42775  aks6d1c6lem2  42800  grpods  42823  unitscyglem1  42824  unitscyglem2  42825  unitscyglem4  42827  mhpind  43188  mhphf  43191  prjcrv0  43227  infdesc  43237  mzpindd  43339  fiphp3d  43408  rencldnfilem  43409  irrapx1  43417  pellexlem3  43420  pellfundre  43470  pellfundge  43471  pellfundlb  43473  pellfundglb  43474  jm2.22  43584  jm2.23  43585  rpnnen3  43621  pwssplit4  43678  pwfi2f1o  43685  hbtlem6  43718  dgraalem  43734  dgraaub  43737  itgocn  43753  onintunirab  43816  nadd2rabord  43974  nadd1rabord  43978  rfovcnvf1od  44592  fsovfd  44600  fsovcnvlem  44601  binomcxplemdvbinom  44927  binomcxplemcvg  44928  binomcxplemnotnn0  44930  uzwo4  45631  disjf1o  45767  icof  45793  allbutfiinf  45992  supminfxr  46036  supminfxr2  46041  fsumsupp0  46152  sumnnodd  46204  fnlimabslt  46251  liminfvalxr  46355  ioodvbdlimc1lem1  46503  dvnprodlem1  46518  dvnprodlem2  46519  stoweidlem14  46586  stoweidlem34  46606  stoweidlem44  46616  stoweidlem50  46622  stoweidlem51  46623  stoweidlem52  46624  stoweidlem57  46629  stoweidlem59  46631  fourierdlem19  46698  fourierdlem20  46699  fourierdlem25  46704  fourierdlem31  46710  fourierdlem37  46716  fourierdlem42  46721  fourierdlem51  46729  fourierdlem54  46732  fourierdlem64  46742  fourierdlem79  46757  elaa2lem  46805  etransclem16  46822  etransclem24  46830  etransclem31  46837  etransclem33  46839  etransclem34  46840  etransclem48  46854  salgencl  46904  salexct  46906  salgenuni  46909  subsaliuncllem  46929  meadjiunlem  47037  caragenss  47076  caratheodory  47100  ovnlecvr  47130  ovnlerp  47134  ovn0lem  47137  ovnsubaddlem1  47142  hoidmv1lelem1  47163  hoidmv1lelem3  47165  hoidmvlelem1  47167  hoidmvlelem2  47168  hoidmvlelem3  47169  hoidmvlelem4  47170  ovnhoilem1  47173  ovnhoilem2  47174  ovnlecvr2  47182  ovncvr2  47183  opnvonmbllem2  47205  ovolval4lem1  47221  pimconstlt1  47274  pimgtmnf2  47286  pimdecfgtioc  47287  pimincfltioc  47288  pimdecfgtioo  47289  pimincfltioo  47290  sssmf  47310  incsmflem  47313  smfaddlem1  47335  smfaddlem2  47336  decsmflem  47338  smflimlem1  47343  smflimlem2  47344  smflimlem3  47345  smfrec  47361  smfmullem4  47366  smfdiv  47369  smfsuplem1  47383  smfsuplem3  47385  smfinflem  47389  smflimsuplem1  47392  smflimsuplem7  47398  smfliminflem  47402  sprsymrelfolem1  48096  prmdvdsfmtnof1lem1  48191  prmdvdsfmtnof  48193  perfectALTVlem2  48342  isubgredg  48486  isubgruhgr  48488  isubgrgrim  48549  uhgrimisgrgric  48551  uspgrlimlem1  48608  uspgrlimlem4  48611  uspgrlim  48612  grlimgrtrilem2  48622  oddibas  48793  2zlidl  48860  2zrngbas  48862  2zrng0  48864  isclatd  49612  topclat  49627