Theorem ssrab2 4046

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

Syntax hints:  {crab 3408   ⊆ wss 3917

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-ss 3934

This theorem is referenced by:  ssrab3  4048  ssrabeq  4050  iinrab2  5037  riinrab  5051  rabelpw  5294  rabexgOLD  5296  frminex  5620  wereu2  5638  predres  6315  frpomin  6316  frpoinsg  6319  ssimaex  6949  f1oresrab  7102  weniso  7332  canth  7344  riotacl  7364  riotassuni  7387  onminesb  7772  onminsb  7773  onintrab  7775  onnminsb  7778  onminex  7781  tfisg  7833  tfis  7834  suppssdm  8159  fnsuppres  8173  oeeulem  8568  nnawordex  8604  pmvalg  8813  fineqvlem  9216  ordtypelem3  9480  ordtypelem4  9481  ordtypelem6  9483  hartogs  9504  card2on  9514  wdom2d  9540  oemapvali  9644  frinsg  9711  tz9.12lem1  9747  tz9.12lem3  9749  rankf  9754  cardf2  9903  cardid2  9913  cardmin2  9959  acni3  10007  dfac2a  10090  cofsmo  10229  coftr  10233  fin2i2  10278  isfin2-2  10279  enfin2i  10281  fin1a2lem11  10370  fin1a2lem12  10371  axdc3lem4  10413  ac6  10440  ondomon  10523  alephval2  10532  pwfseqlem1  10618  pwfseqlem3  10620  wunccl  10704  tskmcl  10801  infm3  12149  uzf  12803  nnwos  12881  supminf  12901  zsupss  12903  rpnnen1lem1  12944  rpnnen1lem3  12945  rpnnen1lem5  12947  ixxf  13323  fzf  13479  flval3  13784  rabssnn0fi  13958  expge0  14070  expge1  14071  hashbclem  14424  01sqrexlem3  15217  rlimrege0  15552  incexc2  15811  bitsf  16404  bitsfzolem  16411  sadadd2lem  16436  sadadd3  16438  sadcl  16439  smupf  16455  smuval2  16459  smupvallem  16460  smucl  16461  smueqlem  16467  lcmcllem  16573  lcmn0cl  16574  lcmledvds  16576  lcmfval  16598  lcmfcllem  16602  lcmfn0cl  16603  lcmfledvds  16609  phicl2  16745  phibnd  16748  hashdvds  16752  phiprmpw  16753  phimullem  16756  eulerth  16760  phisum  16768  odzcllem  16770  odzdvds  16773  prmreclem1  16894  prmreclem2  16895  prmreclem3  16896  prmreclem4  16897  prmreclem5  16898  hashbccl  16981  prmgaplem3  17031  prmgaplem4  17032  prdsds  17434  mrcflem  17574  isacs1i  17625  wunnat  17928  dmcoass  18035  lublecl  18327  lubid  18328  rabsubmgmd  18638  mgmhmeql  18650  issubmd  18740  mhmeql  18760  cntzval  19260  cntzssv  19267  symgsssg  19404  symgfisg  19405  pmtrdifellem4  19416  odfval  19469  odlem1  19472  odlem2  19476  odngen  19514  gexlem1  19516  gexlem2  19519  sylow2alem2  19555  sylow2blem3  19559  oddvdssubg  19792  cyggex2  19834  ablfaclem3  20026  rgspncl  20529  lssacs  20880  lspf  20887  ocvfval  21582  ocvval  21583  dsmmval2  21652  dsmmsubg  21659  asplss  21790  aspsubrg  21792  psrass1lem  21848  psrdi  21881  psrdir  21882  psrass23l  21883  psrass23  21885  resspsrmul  21892  mplbas  21906  mplsubglem  21915  mplsubrglem  21920  mplmonmul  21950  psropprmul  22129  scmatlss  22419  smadiadet  22564  pmatcoe1fsupp  22595  cpmatsubgpmat  22614  fctop  22898  cctop  22900  ppttop  22901  epttop  22903  clscld  22941  neips  23007  neiptopnei  23026  ordtbaslem  23082  ordtuni  23084  ordtcld1  23091  ordtcld2  23092  cnpfval  23128  iscnp2  23133  cmpcov2  23284  cmpsublem  23293  tgcmp  23295  conncompcld  23328  1stcfb  23339  2ndc1stc  23345  2ndcdisj  23350  finlocfin  23414  kgentopon  23432  xkotf  23479  txkgen  23546  xkococnlem  23553  imastopn  23614  kqffn  23619  opnfbas  23736  flimfnfcls  23922  alexsubALT  23945  ptcmplem2  23947  symgtgp  24000  tgpconncompeqg  24006  tgpconncomp  24007  ghmcnp  24009  tsmsfbas  24022  eltsms  24027  utoptop  24129  utopbas  24130  blfvalps  24278  blfps  24301  blf  24302  nmoffn  24606  nmofval  24609  nmogelb  24611  nmolb  24612  nmof  24614  ishtpy  24878  clsocv  25157  rrxnm  25298  rrxbasefi  25317  minveclem3b  25335  minveclem4  25339  ovolcl  25386  ovollb  25387  ovolgelb  25388  ovolge0  25389  ovolshftlem1  25417  ovolshft  25419  ovolscalem1  25421  ovolscalem2  25422  ovolsca  25423  ovolicc2lem3  25427  shftmbl  25446  iundisj  25456  dyadmax  25506  dyadmbllem  25507  opnmbllem  25509  mdegmullem  25990  uc1pval  26052  mon1pval  26054  elqaalem1  26234  elqaalem3  26236  aannenlem2  26244  aalioulem2  26248  radcnvcl  26333  radcnvlt1  26334  radcnvle  26336  ftalem4  26993  ftalem5  26994  efnnfsumcl  27020  isppw  27031  sgmval2  27060  efchtdvds  27076  sqff1o  27099  fsumdvdsdiaglem  27100  fsumdvdsdiag  27101  fsumdvdscom  27102  musum  27108  muinv  27110  sgmmul  27119  ppiub  27122  vmasum  27134  logfac2  27135  perfectlem2  27148  lgsfcl  27223  lgscl  27229  lgsquadlem1  27298  lgsquadlem2  27299  rpvmasumlem  27405  mudivsum  27448  mulogsum  27450  mulog2sumlem2  27453  vmalogdivsum2  27456  logsqvma  27460  logsqvma2  27461  selberglem3  27465  selberg  27466  selberg34r  27489  pntsval2  27494  pntrlog2bndlem1  27495  sltval2  27575  conway  27718  eqscut2  27725  scutun12  27729  scutbdaybnd  27734  scutbdaybnd2  27735  scutbdaylt  27737  bday1s  27750  cuteq0  27751  madef  27771  leftssold  27797  rightssold  27798  madebdaylemlrcut  27817  cofcut1  27835  cofcutr  27839  cutlt  27847  precsexlem8  28123  precsexlem11  28126  onssno  28162  onscutlt  28172  onsiso  28176  bdayon  28180  bdayn0p1  28265  tglnunirn  28482  tglnssp  28486  incistruhgr  29013  upgrss  29022  upgrn0  29023  upgruhgr  29036  usgrss  29108  uspgrushgr  29111  ushgredgedg  29163  ushgredgedgloop  29165  vtxdun  29416  vtxdginducedm1  29478  wlknwwlksnbij  29825  hashwwlksnext  29851  frcond3  30205  numclwlk1lem2  30306  ocsh  31219  spancl  31272  shsval2i  31323  ococin  31344  chsupid  31348  speccl  31835  hatomistici  32298  chpssati  32299  iundisjf  32525  aciunf1  32594  fpwrelmap  32663  iundisjfi  32726  pwrssmgc  32933  cycpmco2f1  33088  cycpmco2rn  33089  cycpmco2lem1  33090  cycpmco2lem2  33091  cycpmco2lem3  33092  cycpmco2lem4  33093  cycpmco2lem5  33094  cycpmco2lem6  33095  cycpmco2lem7  33096  cycpmco2  33097  fxpss  33130  nsgmgclem  33389  constrsuc  33735  locfinreflem  33837  zarclsiin  33868  zarcls  33871  zartopn  33872  esumrnmpt2  34065  esumpinfval  34070  sigagensiga  34138  ldgenpisyslem1  34160  ldgenpisys  34163  measvuni  34211  imambfm  34260  dya2iocuni  34281  omscl  34293  oms0  34295  omsmon  34296  omssubadd  34298  carsgcl  34302  oddpwdc  34352  eulerpartlem1  34365  eulerpartlemt  34369  eulerpartgbij  34370  eulerpartlemmf  34373  eulerpartlemgh  34376  eulerpartlemgs2  34378  ballotlem2  34487  ballotlemfc0  34491  ballotlemfcc  34492  ballotlemfmpn  34493  ballotlemiex  34500  ballotlemsup  34503  ballotlem7  34534  ballotth  34536  reprpmtf1o  34624  breprexplema  34628  hgt750lema  34655  bnj110  34855  bnj1204  35009  bnj1311  35021  fnrelpredd  35086  subfacp1lem6  35179  erdszelem2  35186  connpconn  35229  cvmliftmolem2  35276  cvmliftlem15  35292  cvmlift2lem12  35308  snmlff  35323  satfrnmapom  35364  rankeq1o  36166  finminlem  36313  fnessref  36352  neibastop1  36354  neibastop2lem  36355  weiunlem2  36458  weiunse  36463  bj-rabtr  36925  bj-rabtrAUTO  36927  bj-vecssmod  37276  icoreresf  37347  phpreu  37605  fin2so  37608  poimirlem26  37647  poimirlem31  37652  poimirlem32  37653  opnmbllem0  37657  mblfinlem1  37658  mblfinlem2  37659  ismblfin  37662  mbfposadd  37668  cnambfre  37669  cover2  37716  indexa  37734  fdc  37746  sstotbnd2  37775  sstotbnd3  37777  igenidl  38064  prnc  38068  toycom  38973  lkrlss  39095  atlatmstc  39319  atlatle  39320  glbconN  39377  glbconNOLD  39378  linepsubN  39753  pmapssat  39760  pmaple  39762  pmapsub  39769  paddssat  39815  diass  41043  diaglbN  41056  diaintclN  41059  diassdvaN  41061  docaclN  41125  dibglbN  41167  dibintclN  41168  diclspsn  41195  dihglblem2N  41295  dih1dimatlem  41330  dihglb2  41343  dochval2  41353  dochcl  41354  dochvalr  41358  doch2val2  41365  dochss  41366  dochocss  41367  lclkr  41534  lclkrs  41540  lcdvbase  41594  lcdvbasess  41595  mapdunirnN  41651  aks4d1p4  42074  aks4d1p5  42075  aks4d1p7  42078  aks4d1p8  42082  sticksstones1  42141  aks6d1c6lem2  42166  grpods  42189  unitscyglem1  42190  unitscyglem2  42191  unitscyglem4  42193  mhpind  42589  mhphf  42592  prjcrv0  42628  infdesc  42638  mzpindd  42741  fiphp3d  42814  rencldnfilem  42815  irrapx1  42823  pellexlem3  42826  pellfundre  42876  pellfundge  42877  pellfundlb  42879  pellfundglb  42880  jm2.22  42991  jm2.23  42992  rpnnen3  43028  pwssplit4  43085  pwfi2f1o  43092  hbtlem6  43125  dgraalem  43141  dgraaub  43144  itgocn  43160  onintunirab  43223  nadd2rabord  43381  nadd1rabord  43385  rfovcnvf1od  44000  fsovfd  44008  fsovcnvlem  44009  binomcxplemdvbinom  44349  binomcxplemcvg  44350  binomcxplemnotnn0  44352  uzwo4  45054  disjf1o  45192  icof  45220  allbutfiinf  45423  supminfxr  45467  supminfxr2  45472  fsumsupp0  45583  sumnnodd  45635  fnlimabslt  45684  liminfvalxr  45788  ioodvbdlimc1lem1  45936  dvnprodlem1  45951  dvnprodlem2  45952  stoweidlem14  46019  stoweidlem34  46039  stoweidlem44  46049  stoweidlem50  46055  stoweidlem51  46056  stoweidlem52  46057  stoweidlem57  46062  stoweidlem59  46064  fourierdlem19  46131  fourierdlem20  46132  fourierdlem25  46137  fourierdlem31  46143  fourierdlem37  46149  fourierdlem42  46154  fourierdlem51  46162  fourierdlem54  46165  fourierdlem64  46175  fourierdlem79  46190  elaa2lem  46238  etransclem16  46255  etransclem24  46263  etransclem31  46270  etransclem33  46272  etransclem34  46273  etransclem48  46287  salgencl  46337  salexct  46339  salgenuni  46342  subsaliuncllem  46362  meadjiunlem  46470  caragenss  46509  caratheodory  46533  ovnlecvr  46563  ovnlerp  46567  ovn0lem  46570  ovnsubaddlem1  46575  hoidmv1lelem1  46596  hoidmv1lelem3  46598  hoidmvlelem1  46600  hoidmvlelem2  46601  hoidmvlelem3  46602  hoidmvlelem4  46603  ovnhoilem1  46606  ovnhoilem2  46607  ovnlecvr2  46615  ovncvr2  46616  opnvonmbllem2  46638  ovolval4lem1  46654  pimconstlt1  46707  pimiooltgt  46715  pimgtmnf2  46719  pimdecfgtioc  46720  pimincfltioc  46721  pimdecfgtioo  46722  pimincfltioo  46723  sssmf  46743  incsmflem  46746  smfaddlem1  46768  smfaddlem2  46769  decsmflem  46771  smflimlem1  46776  smflimlem2  46777  smflimlem3  46778  smfrec  46794  smfmullem4  46799  smfdiv  46802  smfsuplem1  46816  smfsuplem3  46818  smfinflem  46822  smflimsuplem1  46825  smflimsuplem7  46831  smfliminflem  46835  sprsymrelfolem1  47497  prmdvdsfmtnof1lem1  47589  prmdvdsfmtnof  47591  perfectALTVlem2  47727  isubgredg  47870  isubgruhgr  47872  isubgrgrim  47933  uhgrimisgrgric  47935  uspgrlimlem1  47991  uspgrlimlem4  47994  uspgrlim  47995  grlimgrtrilem2  47998  oddibas  48165  2zlidl  48232  2zrngbas  48234  2zrng0  48236  isclatd  48975  topclat  48990