Theorem ssrab2 4028

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 3935	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴

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

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-ss 3916

This theorem is used by:  ssrab3  4030  ssrabeq  4032  iinrab2  5028  riinrab  5044  rabelpw  5301  frminex  5634  wereu2  5652  predres  6337  frpomin  6338  frpoinsg  6341  ssimaex  6963  f1oresrab  7121  weniso  7357  canth  7367  riotacl  7387  riotassuni  7410  onminesb  7792  onminsb  7793  onintrab  7795  onnminsb  7798  onminex  7801  tfisg  7850  tfis  7851  suppssdm  8175  fnsuppres  8189  oeeulem  8589  nnawordex  8625  pmvalg  8836  fineqvlem  9236  ordtypelem3  9492  ordtypelem4  9493  ordtypelem6  9495  hartogs  9516  card2on  9526  wdom2d  9552  oemapvali  9663  frinsg  9733  tz9.12lem1  9769  tz9.12lem3  9771  rankf  9776  cardf2  9948  cardid2  9958  cardmin2  10004  acni3  10050  dfac2a  10132  cofsmo  10271  coftr  10275  fin2i2  10320  isfin2-2  10321  enfin2i  10323  fin1a2lem11  10412  fin1a2lem12  10413  axdc3lem4  10455  ac6  10482  ondomon  10571  alephval2  10581  pwfseqlem1  10667  pwfseqlem3  10669  wunccl  10753  tskmcl  10850  infm3  12198  uzf  12890  nnwos  12964  supminf  12984  zsupss  12986  rpnnen1lem1  13028  rpnnen1lem3  13029  rpnnen1lem5  13031  ixxf  13408  fzf  13565  flval3  13876  rabssnn0fi  14050  expge0  14162  expge1  14163  hashbclem  14517  01sqrexlem3  15331  rlimrege0  15666  incexc2  15927  bitsf  16517  bitsfzolem  16524  sadadd2lem  16549  sadadd3  16551  sadcl  16552  smupf  16568  smuval2  16572  smupvallem  16573  smucl  16574  smueqlem  16580  lcmcllem  16686  lcmn0cl  16687  lcmledvds  16689  lcmfval  16711  lcmfcllem  16715  lcmfn0cl  16716  lcmfledvds  16722  phicl2  16859  phibnd  16862  hashdvds  16866  phiprmpw  16867  phimullem  16870  eulerth  16874  phisum  16882  odzcllem  16884  odzdvds  16887  prmreclem1  17008  prmreclem2  17009  prmreclem3  17010  prmreclem4  17011  prmreclem5  17012  hashbccl  17095  prmgaplem3  17145  prmgaplem4  17146  prdsds  17549  mrcflem  17694  isacs1i  17745  wunnat  18048  dmcoass  18155  lublecl  18447  lubid  18448  rabsubmgmd  18806  mgmhmeql  18818  issubmd  18914  mhmeql  18935  cntzval  19448  cntzssv  19455  symgsssg  19594  symgfisg  19595  pmtrdifellem4  19606  odfval  19659  odlem1  19662  odlem2  19666  odngen  19704  gexlem1  19706  gexlem2  19709  sylow2alem2  19745  sylow2blem3  19749  oddvdssubg  19982  cyggex2  20024  ablfaclem3  20216  rgspncl  20775  lssacs  21151  lspf  21158  ocvfval  21879  ocvval  21880  dsmmval2  21949  dsmmsubg  21956  asplss  22088  aspsubrg  22090  psrass1lem  22148  psrdi  22179  psrdir  22180  psrass23l  22181  psrass23  22183  resspsrmul  22190  mplbas  22204  mplsubglem  22213  mplsubrglem  22218  mplmonmul  22252  psropprmul  22462  scmatlss  22747  smadiadet  22892  pmatcoe1fsupp  22926  cpmatsubgpmat  22945  fctop  23229  cctop  23231  ppttop  23232  epttop  23234  clscld  23272  neips  23338  neiptopnei  23357  ordtbaslem  23413  ordtuni  23415  ordtcld1  23422  ordtcld2  23423  cnpfval  23459  iscnp2  23464  cmpcov2  23615  cmpsublem  23624  tgcmp  23626  conncompcld  23659  1stcfb  23670  2ndc1stc  23676  2ndcdisj  23682  finlocfin  23746  kgentopon  23764  xkotf  23811  txkgen  23878  xkococnlem  23885  imastopn  23946  kqffn  23951  opnfbas  24068  flimfnfcls  24254  alexsubALT  24277  ptcmplem2  24279  symgtgp  24332  tgpconncompeqg  24338  tgpconncomp  24339  ghmcnp  24341  tsmsfbas  24354  eltsms  24359  utoptop  24460  utopbas  24461  blfvalps  24609  blfps  24632  blf  24633  nmoffn  24937  nmofval  24940  nmogelb  24942  nmolb  24943  nmof  24945  ishtpy  25200  clsocv  25478  rrxnm  25619  rrxbasefi  25638  minveclem3b  25656  minveclem4  25660  ovolcl  25706  ovollb  25707  ovolgelb  25708  ovolge0  25709  ovolshftlem1  25737  ovolshft  25739  ovolscalem1  25741  ovolscalem2  25742  ovolsca  25743  ovolicc2lem3  25747  shftmbl  25766  iundisj  25776  dyadmax  25826  dyadmbllem  25827  opnmbllem  25829  mdegmullem  26303  uc1pval  26365  mon1pval  26367  elqaalem1  26551  elqaalem3  26553  aannenlem2  26565  aalioulem2  26569  radcnvcl  26653  radcnvlt1  26654  radcnvle  26656  ftalem4  27312  ftalem5  27313  efnnfsumcl  27339  isppw  27350  sgmval2  27379  efchtdvds  27395  sqff1o  27418  fsumdvdsdiaglem  27419  fsumdvdsdiag  27420  fsumdvdscom  27421  musum  27427  muinv  27429  sgmmul  27437  ppiub  27440  vmasum  27452  logfac2  27453  perfectlem2  27466  lgsfcl  27541  lgscl  27547  lgsquadlem1  27616  lgsquadlem2  27617  rpvmasumlem  27723  mudivsum  27766  mulogsum  27768  mulog2sumlem2  27771  vmalogdivsum2  27774  logsqvma  27778  logsqvma2  27779  selberglem3  27783  selberg  27784  selberg34r  27807  pntsval2  27812  pntrlog2bndlem1  27813  ltsval2  27892  conway  28044  eqcuts2  28051  cutsun12  28055  cutbdaybnd  28060  cutbdaybnd2  28061  cutbdaylt  28063  bday1  28079  cuteq0  28080  madef  28101  leftssold  28136  rightssold  28137  madebdaylemlrcut  28164  sltsbday  28182  cofcut1  28185  cofcutr  28189  cutlt  28197  precsexlem8  28479  precsexlem11  28482  onssno  28519  oncutlt  28529  oniso  28536  bdayons  28541  bdayn0p1  28634  tglnunirn  28890  tglnssp  28894  plngrnssp  29136  plngssp  29138  incistruhgr  29536  upgrss  29545  upgrn0  29546  upgruhgr  29559  usgrss  29634  uspgrushgr  29637  ushgredgedg  29689  ushgredgedgloop  29691  vtxdun  29941  vtxdginducedm1  30003  wlknwwlksnbij  30356  hashwwlksnext  30382  frcond3  30749  numclwlk1lem2  30850  ocsh  31764  spancl  31817  shsval2i  31868  ococin  31889  chsupid  31893  speccl  32380  hatomistici  32843  chpssati  32844  iundisjf  33062  aciunf1  33136  fpwrelmap  33204  iundisjfi  33267  pwrssmgc  33440  cycpmco2f1  33564  cycpmco2rn  33565  cycpmco2lem1  33566  cycpmco2lem2  33567  cycpmco2lem3  33568  cycpmco2lem4  33569  cycpmco2lem5  33570  cycpmco2lem6  33571  cycpmco2lem7  33572  cycpmco2  33573  fxpss  33606  nsgmgclem  33840  0mplrim  34024  selvply1rhmlemb  34029  selvply1rhm0  34036  extvfvcl  34046  mplmulmvr  34049  evlextv  34052  mplvrpmlem  34053  mplvrpmga  34055  mplvrpmrhm  34057  psrmonmul  34060  esplylem  34076  esplympl  34077  esplymhp  34078  esplyfv1  34079  esplyfv  34080  esplyfval3  34082  esplyfval1  34083  esplyfvaln  34084  constrsuc  34248  locfinreflem  34350  zarclsiin  34381  zarcls  34384  zartopn  34385  esumrnmpt2  34578  esumpinfval  34583  sigagensiga  34652  ldgenpisyslem1  34674  ldgenpisys  34677  measvuni  34725  imambfm  34773  dya2iocuni  34794  omscl  34806  oms0  34808  omsmon  34809  omssubadd  34811  carsgcl  34815  oddpwdc  34865  eulerpartlem1  34878  eulerpartlemt  34882  eulerpartgbij  34883  eulerpartlemmf  34886  eulerpartlemgh  34889  eulerpartlemgs2  34891  ballotlem2  35000  ballotlemfc0  35004  ballotlemfcc  35005  ballotlemfmpn  35006  ballotlemiex  35013  ballotlemsup  35016  ballotlem7  35047  ballotth  35049  reprpmtf1o  35134  breprexplema  35138  hgt750lema  35165  bnj110  35367  bnj1204  35521  bnj1311  35533  fnrelpredd  35596  subfacp1lem6  35764  erdszelem2  35771  connpconn  35814  cvmliftmolem2  35861  cvmliftlem15  35877  cvmlift2lem12  35893  snmlff  35908  satfrnmapom  35949  rankeq1o  36751  nmuladdel  36792  finminlem  36937  fnessref  36976  neibastop1  36978  neibastop2lem  36979  weiunlem  37082  weiunse  37087  bj-rabtr  37674  bj-rabtrAUTO  37676  bj-vecssmod  38033  icoreresf  38106  phpreu  38358  fin2so  38361  poimirlem26  38395  poimirlem31  38400  poimirlem32  38401  opnmbllem0  38405  mblfinlem1  38406  mblfinlem2  38407  ismblfin  38410  mbfposadd  38416  cnambfre  38417  cover2  38465  indexa  38483  fdc  38495  sstotbnd2  38524  sstotbnd3  38526  igenidl  38813  prnc  38817  toycom  39846  lkrlss  39968  atlatmstc  40192  atlatle  40193  glbconN  40250  linepsubN  40625  pmapssat  40632  pmaple  40634  pmapsub  40641  paddssat  40687  diass  41915  diaglbN  41928  diaintclN  41931  diassdvaN  41933  docaclN  41997  dibglbN  42039  dibintclN  42040  diclspsn  42067  dihglblem2N  42167  dih1dimatlem  42202  dihglb2  42215  dochval2  42225  dochcl  42226  dochvalr  42230  doch2val2  42237  dochss  42238  dochocss  42239  lclkr  42406  lclkrs  42412  lcdvbase  42466  lcdvbasess  42467  mapdunirnN  42523  aks4d1p4  42945  aks4d1p5  42946  aks4d1p7  42949  aks4d1p8  42953  sticksstones1  43012  aks6d1c6lem2  43037  grpods  43060  unitscyglem1  43061  unitscyglem2  43062  unitscyglem4  43064  mhpind  43440  mhphf  43443  prjcrv0  43479  infdesc  43489  mzpindd  43591  fiphp3d  43660  rencldnfilem  43661  irrapx1  43669  pellexlem3  43672  pellfundre  43722  pellfundge  43723  pellfundlb  43725  pellfundglb  43726  jm2.22  43836  jm2.23  43837  rpnnen3  43873  pwssplit4  43930  pwfi2f1o  43937  hbtlem6  43970  dgraalem  43986  dgraaub  43989  itgocn  44005  onintunirab  44068  nadd2rabord  44226  nadd1rabord  44230  rfovcnvf1od  44844  fsovfd  44852  fsovcnvlem  44853  binomcxplemdvbinom  45177  binomcxplemcvg  45178  binomcxplemnotnn0  45180  uzwo4  45887  disjf1o  46023  icof  46049  allbutfiinf  46248  supminfxr  46292  supminfxr2  46297  fsumsupp0  46408  sumnnodd  46460  fnlimabslt  46507  liminfvalxr  46611  ioodvbdlimc1lem1  46759  dvnprodlem1  46774  dvnprodlem2  46775  stoweidlem14  46842  stoweidlem34  46862  stoweidlem44  46872  stoweidlem50  46878  stoweidlem51  46879  stoweidlem52  46880  stoweidlem57  46885  stoweidlem59  46887  fourierdlem19  46954  fourierdlem20  46955  fourierdlem25  46960  fourierdlem31  46966  fourierdlem37  46972  fourierdlem42  46977  fourierdlem51  46985  fourierdlem54  46988  fourierdlem64  46998  fourierdlem79  47013  elaa2lem  47061  etransclem16  47078  etransclem24  47086  etransclem31  47093  etransclem33  47095  etransclem34  47096  etransclem48  47110  salgencl  47160  salexct  47162  salgenuni  47165  subsaliuncllem  47185  meadjiunlem  47293  caragenss  47332  caratheodory  47356  ovnlecvr  47386  ovnlerp  47390  ovn0lem  47393  ovnsubaddlem1  47398  hoidmv1lelem1  47419  hoidmv1lelem3  47421  hoidmvlelem1  47423  hoidmvlelem2  47424  hoidmvlelem3  47425  hoidmvlelem4  47426  ovnhoilem1  47429  ovnhoilem2  47430  ovnlecvr2  47438  ovncvr2  47439  opnvonmbllem2  47461  ovolval4lem1  47477  pimconstlt1  47530  pimgtmnf2  47542  pimdecfgtioc  47543  pimincfltioc  47544  pimdecfgtioo  47545  pimincfltioo  47546  sssmf  47566  incsmflem  47569  smfaddlem1  47591  smfaddlem2  47592  decsmflem  47594  smflimlem1  47599  smflimlem2  47600  smflimlem3  47601  smfrec  47617  smfmullem4  47622  smfdiv  47625  smfpimcclem  47635  smfsuplem1  47639  smfsuplem3  47641  smfinflem  47645  smflimsuplem1  47648  smflimsuplem7  47654  smfliminflem  47658  tmachlem-agreeself  47764  tmachlem-agreeprod  47765  tmachlem-uassst  47771  tmachlem-extpcover  47773  tmachlem-agreefin  47776  sprsymrelfolem1  48392  prmdvdsfmtnof1lem1  48487  prmdvdsfmtnof  48489  perfectALTVlem2  48638  isubgredg  48782  isubgruhgr  48784  isubgrgrim  48845  uhgrimisgrgric  48847  uspgrlimlem1  48904  uspgrlimlem4  48907  uspgrlim  48908  grlimgrtrilem2  48918  oddibas  49088  2zlidl  49155  2zrngbas  49157  2zrng0  49159  isclatd  49909  topclat  49924  dvsec  50689  dvcsc  50690  dvcot  50691