Theorem ssrab2 4035

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

Syntax hints:  {crab 3416   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-ss 3923

This theorem is referenced by:  ssrab3  4037  ssrabeq  4039  iinrab2  5035  riinrab  5051  rabelpw  5308  rabexgOLD  5310  frminex  5642  wereu2  5660  predres  6342  frpomin  6343  frpoinsg  6346  ssimaex  6968  f1oresrab  7125  weniso  7354  canth  7366  riotacl  7386  riotassuni  7409  onminesb  7793  onminsb  7794  onintrab  7796  onnminsb  7799  onminex  7802  tfisg  7851  tfis  7852  suppssdm  8174  fnsuppres  8188  oeeulem  8588  nnawordex  8624  pmvalg  8835  fineqvlem  9227  ordtypelem3  9483  ordtypelem4  9484  ordtypelem6  9486  hartogs  9507  card2on  9517  wdom2d  9543  oemapvali  9654  frinsg  9724  tz9.12lem1  9760  tz9.12lem3  9762  rankf  9767  cardf2  9930  cardid2  9940  cardmin2  9986  acni3  10032  dfac2a  10114  cofsmo  10254  coftr  10258  fin2i2  10303  isfin2-2  10304  enfin2i  10306  fin1a2lem11  10395  fin1a2lem12  10396  axdc3lem4  10438  ac6  10465  ondomon  10548  alephval2  10558  pwfseqlem1  10644  pwfseqlem3  10646  wunccl  10730  tskmcl  10827  infm3  12175  uzf  12866  nnwos  12940  supminf  12960  zsupss  12962  rpnnen1lem1  13003  rpnnen1lem3  13004  rpnnen1lem5  13006  ixxf  13383  fzf  13540  flval3  13850  rabssnn0fi  14024  expge0  14136  expge1  14137  hashbclem  14491  01sqrexlem3  15297  rlimrege0  15632  incexc2  15894  bitsf  16486  bitsfzolem  16493  sadadd2lem  16518  sadadd3  16520  sadcl  16521  smupf  16537  smuval2  16541  smupvallem  16542  smucl  16543  smueqlem  16549  lcmcllem  16655  lcmn0cl  16656  lcmledvds  16658  lcmfval  16680  lcmfcllem  16684  lcmfn0cl  16685  lcmfledvds  16691  phicl2  16828  phibnd  16831  hashdvds  16835  phiprmpw  16836  phimullem  16839  eulerth  16843  phisum  16851  odzcllem  16853  odzdvds  16856  prmreclem1  16977  prmreclem2  16978  prmreclem3  16979  prmreclem4  16980  prmreclem5  16981  hashbccl  17064  prmgaplem3  17114  prmgaplem4  17115  prdsds  17518  mrcflem  17663  isacs1i  17714  wunnat  18017  dmcoass  18124  lublecl  18416  lubid  18417  rabsubmgmd  18763  mgmhmeql  18775  issubmd  18865  mhmeql  18886  cntzval  19392  cntzssv  19399  symgsssg  19538  symgfisg  19539  pmtrdifellem4  19550  odfval  19603  odlem1  19606  odlem2  19610  odngen  19648  gexlem1  19650  gexlem2  19653  sylow2alem2  19689  sylow2blem3  19693  oddvdssubg  19926  cyggex2  19968  ablfaclem3  20160  rgspncl  20699  lssacs  21069  lspf  21076  ocvfval  21797  ocvval  21798  dsmmval2  21867  dsmmsubg  21874  asplss  22004  aspsubrg  22006  psrass1lem  22064  psrdi  22095  psrdir  22096  psrass23l  22097  psrass23  22099  resspsrmul  22106  mplbas  22120  mplsubglem  22129  mplsubrglem  22134  mplmonmul  22168  psropprmul  22378  scmatlss  22663  smadiadet  22808  pmatcoe1fsupp  22839  cpmatsubgpmat  22858  fctop  23142  cctop  23144  ppttop  23145  epttop  23147  clscld  23185  neips  23251  neiptopnei  23270  ordtbaslem  23326  ordtuni  23328  ordtcld1  23335  ordtcld2  23336  cnpfval  23372  iscnp2  23377  cmpcov2  23528  cmpsublem  23537  tgcmp  23539  conncompcld  23572  1stcfb  23583  2ndc1stc  23589  2ndcdisj  23594  finlocfin  23658  kgentopon  23676  xkotf  23723  txkgen  23790  xkococnlem  23797  imastopn  23858  kqffn  23863  opnfbas  23980  flimfnfcls  24166  alexsubALT  24189  ptcmplem2  24191  symgtgp  24244  tgpconncompeqg  24250  tgpconncomp  24251  ghmcnp  24253  tsmsfbas  24266  eltsms  24271  utoptop  24372  utopbas  24373  blfvalps  24521  blfps  24544  blf  24545  nmoffn  24849  nmofval  24852  nmogelb  24854  nmolb  24855  nmof  24857  ishtpy  25112  clsocv  25390  rrxnm  25531  rrxbasefi  25550  minveclem3b  25568  minveclem4  25572  ovolcl  25618  ovollb  25619  ovolgelb  25620  ovolge0  25621  ovolshftlem1  25649  ovolshft  25651  ovolscalem1  25653  ovolscalem2  25654  ovolsca  25655  ovolicc2lem3  25659  shftmbl  25678  iundisj  25688  dyadmax  25738  dyadmbllem  25739  opnmbllem  25741  mdegmullem  26216  uc1pval  26278  mon1pval  26280  elqaalem1  26461  elqaalem3  26463  aannenlem2  26473  aalioulem2  26477  radcnvcl  26561  radcnvlt1  26562  radcnvle  26564  ftalem4  27221  ftalem5  27222  efnnfsumcl  27248  isppw  27259  sgmval2  27288  efchtdvds  27304  sqff1o  27327  fsumdvdsdiaglem  27328  fsumdvdsdiag  27329  fsumdvdscom  27330  musum  27336  muinv  27338  sgmmul  27346  ppiub  27349  vmasum  27361  logfac2  27362  perfectlem2  27375  lgsfcl  27450  lgscl  27456  lgsquadlem1  27525  lgsquadlem2  27526  rpvmasumlem  27632  mudivsum  27675  mulogsum  27677  mulog2sumlem2  27680  vmalogdivsum2  27683  logsqvma  27687  logsqvma2  27688  selberglem3  27692  selberg  27693  selberg34r  27716  pntsval2  27721  pntrlog2bndlem1  27722  ltsval2  27801  conway  27953  eqcuts2  27960  cutsun12  27964  cutbdaybnd  27969  cutbdaybnd2  27970  cutbdaylt  27972  bday1  27988  cuteq0  27989  madef  28010  leftssold  28045  rightssold  28046  madebdaylemlrcut  28073  sltsbday  28091  cofcut1  28094  cofcutr  28098  cutlt  28106  precsexlem8  28388  precsexlem11  28391  onssno  28428  oncutlt  28438  oniso  28445  bdayons  28450  bdayn0p1  28543  tglnunirn  28798  tglnssp  28802  plngrnssp  29042  plngssp  29044  incistruhgr  29410  upgrss  29419  upgrn0  29420  upgruhgr  29433  usgrss  29505  uspgrushgr  29508  ushgredgedg  29560  ushgredgedgloop  29562  vtxdun  29812  vtxdginducedm1  29874  wlknwwlksnbij  30218  hashwwlksnext  30244  frcond3  30601  numclwlk1lem2  30702  ocsh  31616  spancl  31669  shsval2i  31720  ococin  31741  chsupid  31745  speccl  32232  hatomistici  32695  chpssati  32696  iundisjf  32915  aciunf1  32989  fpwrelmap  33059  iundisjfi  33122  pwrssmgc  33301  cycpmco2f1  33425  cycpmco2rn  33426  cycpmco2lem1  33427  cycpmco2lem2  33428  cycpmco2lem3  33429  cycpmco2lem4  33430  cycpmco2lem5  33431  cycpmco2lem6  33432  cycpmco2lem7  33433  cycpmco2  33434  fxpss  33467  nsgmgclem  33701  0mplrim  33885  selvply1rhmlemb  33890  selvply1rhm0  33897  extvfvcl  33907  mplmulmvr  33910  evlextv  33913  mplvrpmlem  33914  mplvrpmga  33916  mplvrpmrhm  33918  psrmonmul  33921  esplylem  33937  esplympl  33938  esplymhp  33939  esplyfv1  33940  esplyfv  33941  esplyfval3  33943  esplyfval1  33944  esplyfvaln  33945  constrsuc  34109  locfinreflem  34211  zarclsiin  34242  zarcls  34245  zartopn  34246  esumrnmpt2  34439  esumpinfval  34444  sigagensiga  34512  ldgenpisyslem1  34534  ldgenpisys  34537  measvuni  34585  imambfm  34633  dya2iocuni  34654  omscl  34666  oms0  34668  omsmon  34669  omssubadd  34671  carsgcl  34675  oddpwdc  34725  eulerpartlem1  34738  eulerpartlemt  34742  eulerpartgbij  34743  eulerpartlemmf  34746  eulerpartlemgh  34749  eulerpartlemgs2  34751  ballotlem2  34860  ballotlemfc0  34864  ballotlemfcc  34865  ballotlemfmpn  34866  ballotlemiex  34873  ballotlemsup  34876  ballotlem7  34907  ballotth  34909  reprpmtf1o  34994  breprexplema  34998  hgt750lema  35025  bnj110  35227  bnj1204  35381  bnj1311  35393  fnrelpredd  35463  subfacp1lem6  35658  erdszelem2  35665  connpconn  35708  cvmliftmolem2  35755  cvmliftlem15  35771  cvmlift2lem12  35787  snmlff  35802  satfrnmapom  35843  rankeq1o  36644  nmuladdel  36670  finminlem  36810  fnessref  36849  neibastop1  36851  neibastop2lem  36852  weiunlem  36955  weiunse  36960  bj-rabtr  37547  bj-rabtrAUTO  37549  bj-vecssmod  37906  icoreresf  37979  phpreu  38236  fin2so  38239  poimirlem26  38278  poimirlem31  38283  poimirlem32  38284  opnmbllem0  38288  mblfinlem1  38289  mblfinlem2  38290  ismblfin  38293  mbfposadd  38299  cnambfre  38300  cover2  38347  indexa  38365  fdc  38377  sstotbnd2  38406  sstotbnd3  38408  igenidl  38695  prnc  38699  toycom  39728  lkrlss  39850  atlatmstc  40074  atlatle  40075  glbconN  40132  linepsubN  40507  pmapssat  40514  pmaple  40516  pmapsub  40523  paddssat  40569  diass  41797  diaglbN  41810  diaintclN  41813  diassdvaN  41815  docaclN  41879  dibglbN  41921  dibintclN  41922  diclspsn  41949  dihglblem2N  42049  dih1dimatlem  42084  dihglb2  42097  dochval2  42107  dochcl  42108  dochvalr  42112  doch2val2  42119  dochss  42120  dochocss  42121  lclkr  42288  lclkrs  42294  lcdvbase  42348  lcdvbasess  42349  mapdunirnN  42405  aks4d1p4  42827  aks4d1p5  42828  aks4d1p7  42831  aks4d1p8  42835  sticksstones1  42894  aks6d1c6lem2  42919  grpods  42942  unitscyglem1  42943  unitscyglem2  42944  unitscyglem4  42946  mhpind  43309  mhphf  43312  prjcrv0  43348  infdesc  43358  mzpindd  43460  fiphp3d  43529  rencldnfilem  43530  irrapx1  43538  pellexlem3  43541  pellfundre  43591  pellfundge  43592  pellfundlb  43594  pellfundglb  43595  jm2.22  43705  jm2.23  43706  rpnnen3  43742  pwssplit4  43799  pwfi2f1o  43806  hbtlem6  43839  dgraalem  43855  dgraaub  43858  itgocn  43874  onintunirab  43937  nadd2rabord  44095  nadd1rabord  44099  rfovcnvf1od  44713  fsovfd  44721  fsovcnvlem  44722  binomcxplemdvbinom  45046  binomcxplemcvg  45047  binomcxplemnotnn0  45049  uzwo4  45756  disjf1o  45892  icof  45918  allbutfiinf  46117  supminfxr  46161  supminfxr2  46166  fsumsupp0  46277  sumnnodd  46329  fnlimabslt  46376  liminfvalxr  46480  ioodvbdlimc1lem1  46628  dvnprodlem1  46643  dvnprodlem2  46644  stoweidlem14  46711  stoweidlem34  46731  stoweidlem44  46741  stoweidlem50  46747  stoweidlem51  46748  stoweidlem52  46749  stoweidlem57  46754  stoweidlem59  46756  fourierdlem19  46823  fourierdlem20  46824  fourierdlem25  46829  fourierdlem31  46835  fourierdlem37  46841  fourierdlem42  46846  fourierdlem51  46854  fourierdlem54  46857  fourierdlem64  46867  fourierdlem79  46882  elaa2lem  46930  etransclem16  46947  etransclem24  46955  etransclem31  46962  etransclem33  46964  etransclem34  46965  etransclem48  46979  salgencl  47029  salexct  47031  salgenuni  47034  subsaliuncllem  47054  meadjiunlem  47162  caragenss  47201  caratheodory  47225  ovnlecvr  47255  ovnlerp  47259  ovn0lem  47262  ovnsubaddlem1  47267  hoidmv1lelem1  47288  hoidmv1lelem3  47290  hoidmvlelem1  47292  hoidmvlelem2  47293  hoidmvlelem3  47294  hoidmvlelem4  47295  ovnhoilem1  47298  ovnhoilem2  47299  ovnlecvr2  47307  ovncvr2  47308  opnvonmbllem2  47330  ovolval4lem1  47346  pimconstlt1  47399  pimgtmnf2  47411  pimdecfgtioc  47412  pimincfltioc  47413  pimdecfgtioo  47414  pimincfltioo  47415  sssmf  47435  incsmflem  47438  smfaddlem1  47460  smfaddlem2  47461  decsmflem  47463  smflimlem1  47468  smflimlem2  47469  smflimlem3  47470  smfrec  47486  smfmullem4  47491  smfdiv  47494  smfpimcclem  47504  smfsuplem1  47508  smfsuplem3  47510  smfinflem  47514  smflimsuplem1  47517  smflimsuplem7  47523  smfliminflem  47527  sprsymrelfolem1  48224  prmdvdsfmtnof1lem1  48319  prmdvdsfmtnof  48321  perfectALTVlem2  48470  isubgredg  48614  isubgruhgr  48616  isubgrgrim  48677  uhgrimisgrgric  48679  uspgrlimlem1  48736  uspgrlimlem4  48739  uspgrlim  48740  grlimgrtrilem2  48750  oddibas  48921  2zlidl  48988  2zrngbas  48990  2zrng0  48992  isclatd  49744  topclat  49759