Theorem ssrab2 4032

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

Syntax hints:  {crab 3399   ⊆ wss 3901

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 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-ss 3918

This theorem is referenced by:  ssrab3  4034  ssrabeq  4036  iinrab2  5025  riinrab  5039  rabelpw  5281  rabexgOLD  5283  frminex  5603  wereu2  5621  predres  6297  frpomin  6298  frpoinsg  6301  ssimaex  6919  f1oresrab  7072  weniso  7300  canth  7312  riotacl  7332  riotassuni  7355  onminesb  7738  onminsb  7739  onintrab  7741  onnminsb  7744  onminex  7747  tfisg  7796  tfis  7797  suppssdm  8119  fnsuppres  8133  oeeulem  8529  nnawordex  8565  pmvalg  8774  fineqvlem  9166  ordtypelem3  9425  ordtypelem4  9426  ordtypelem6  9428  hartogs  9449  card2on  9459  wdom2d  9485  oemapvali  9593  frinsg  9663  tz9.12lem1  9699  tz9.12lem3  9701  rankf  9706  cardf2  9855  cardid2  9865  cardmin2  9911  acni3  9957  dfac2a  10040  cofsmo  10179  coftr  10183  fin2i2  10228  isfin2-2  10229  enfin2i  10231  fin1a2lem11  10320  fin1a2lem12  10321  axdc3lem4  10363  ac6  10390  ondomon  10473  alephval2  10483  pwfseqlem1  10569  pwfseqlem3  10571  wunccl  10655  tskmcl  10752  infm3  12101  uzf  12754  nnwos  12828  supminf  12848  zsupss  12850  rpnnen1lem1  12891  rpnnen1lem3  12892  rpnnen1lem5  12894  ixxf  13271  fzf  13427  flval3  13735  rabssnn0fi  13909  expge0  14021  expge1  14022  hashbclem  14375  01sqrexlem3  15167  rlimrege0  15502  incexc2  15761  bitsf  16354  bitsfzolem  16361  sadadd2lem  16386  sadadd3  16388  sadcl  16389  smupf  16405  smuval2  16409  smupvallem  16410  smucl  16411  smueqlem  16417  lcmcllem  16523  lcmn0cl  16524  lcmledvds  16526  lcmfval  16548  lcmfcllem  16552  lcmfn0cl  16553  lcmfledvds  16559  phicl2  16695  phibnd  16698  hashdvds  16702  phiprmpw  16703  phimullem  16706  eulerth  16710  phisum  16718  odzcllem  16720  odzdvds  16723  prmreclem1  16844  prmreclem2  16845  prmreclem3  16846  prmreclem4  16847  prmreclem5  16848  hashbccl  16931  prmgaplem3  16981  prmgaplem4  16982  prdsds  17384  mrcflem  17529  isacs1i  17580  wunnat  17883  dmcoass  17990  lublecl  18282  lubid  18283  rabsubmgmd  18629  mgmhmeql  18641  issubmd  18731  mhmeql  18751  cntzval  19250  cntzssv  19257  symgsssg  19396  symgfisg  19397  pmtrdifellem4  19408  odfval  19461  odlem1  19464  odlem2  19468  odngen  19506  gexlem1  19508  gexlem2  19511  sylow2alem2  19547  sylow2blem3  19551  oddvdssubg  19784  cyggex2  19826  ablfaclem3  20018  rgspncl  20546  lssacs  20918  lspf  20925  ocvfval  21621  ocvval  21622  dsmmval2  21691  dsmmsubg  21698  asplss  21829  aspsubrg  21831  psrass1lem  21888  psrdi  21920  psrdir  21921  psrass23l  21922  psrass23  21924  resspsrmul  21931  mplbas  21945  mplsubglem  21954  mplsubrglem  21959  mplmonmul  21991  psropprmul  22178  scmatlss  22469  smadiadet  22614  pmatcoe1fsupp  22645  cpmatsubgpmat  22664  fctop  22948  cctop  22950  ppttop  22951  epttop  22953  clscld  22991  neips  23057  neiptopnei  23076  ordtbaslem  23132  ordtuni  23134  ordtcld1  23141  ordtcld2  23142  cnpfval  23178  iscnp2  23183  cmpcov2  23334  cmpsublem  23343  tgcmp  23345  conncompcld  23378  1stcfb  23389  2ndc1stc  23395  2ndcdisj  23400  finlocfin  23464  kgentopon  23482  xkotf  23529  txkgen  23596  xkococnlem  23603  imastopn  23664  kqffn  23669  opnfbas  23786  flimfnfcls  23972  alexsubALT  23995  ptcmplem2  23997  symgtgp  24050  tgpconncompeqg  24056  tgpconncomp  24057  ghmcnp  24059  tsmsfbas  24072  eltsms  24077  utoptop  24178  utopbas  24179  blfvalps  24327  blfps  24350  blf  24351  nmoffn  24655  nmofval  24658  nmogelb  24660  nmolb  24661  nmof  24663  ishtpy  24927  clsocv  25206  rrxnm  25347  rrxbasefi  25366  minveclem3b  25384  minveclem4  25388  ovolcl  25435  ovollb  25436  ovolgelb  25437  ovolge0  25438  ovolshftlem1  25466  ovolshft  25468  ovolscalem1  25470  ovolscalem2  25471  ovolsca  25472  ovolicc2lem3  25476  shftmbl  25495  iundisj  25505  dyadmax  25555  dyadmbllem  25556  opnmbllem  25558  mdegmullem  26039  uc1pval  26101  mon1pval  26103  elqaalem1  26283  elqaalem3  26285  aannenlem2  26293  aalioulem2  26297  radcnvcl  26382  radcnvlt1  26383  radcnvle  26385  ftalem4  27042  ftalem5  27043  efnnfsumcl  27069  isppw  27080  sgmval2  27109  efchtdvds  27125  sqff1o  27148  fsumdvdsdiaglem  27149  fsumdvdsdiag  27150  fsumdvdscom  27151  musum  27157  muinv  27159  sgmmul  27168  ppiub  27171  vmasum  27183  logfac2  27184  perfectlem2  27197  lgsfcl  27272  lgscl  27278  lgsquadlem1  27347  lgsquadlem2  27348  rpvmasumlem  27454  mudivsum  27497  mulogsum  27499  mulog2sumlem2  27502  vmalogdivsum2  27505  logsqvma  27509  logsqvma2  27510  selberglem3  27514  selberg  27515  selberg34r  27538  pntsval2  27543  pntrlog2bndlem1  27544  ltsval2  27624  conway  27775  eqcuts2  27782  cutsun12  27786  cutbdaybnd  27791  cutbdaybnd2  27792  cutbdaylt  27794  bday1  27810  cuteq0  27811  madef  27832  leftssold  27867  rightssold  27868  madebdaylemlrcut  27895  sltsbday  27913  cofcut1  27916  cofcutr  27920  cutlt  27928  precsexlem8  28210  precsexlem11  28213  onssno  28250  oncutlt  28260  oniso  28267  bdayons  28272  bdayn0p1  28365  tglnunirn  28620  tglnssp  28624  incistruhgr  29152  upgrss  29161  upgrn0  29162  upgruhgr  29175  usgrss  29247  uspgrushgr  29250  ushgredgedg  29302  ushgredgedgloop  29304  vtxdun  29555  vtxdginducedm1  29617  wlknwwlksnbij  29961  hashwwlksnext  29987  frcond3  30344  numclwlk1lem2  30445  ocsh  31358  spancl  31411  shsval2i  31462  ococin  31483  chsupid  31487  speccl  31974  hatomistici  32437  chpssati  32438  iundisjf  32664  aciunf1  32741  fpwrelmap  32812  iundisjfi  32876  pwrssmgc  33082  cycpmco2f1  33206  cycpmco2rn  33207  cycpmco2lem1  33208  cycpmco2lem2  33209  cycpmco2lem3  33210  cycpmco2lem4  33211  cycpmco2lem5  33212  cycpmco2lem6  33213  cycpmco2lem7  33214  cycpmco2  33215  fxpss  33248  nsgmgclem  33492  extvfvcl  33701  mplmulmvr  33704  evlextv  33707  mplvrpmlem  33708  mplvrpmga  33710  mplvrpmrhm  33712  esplylem  33724  esplympl  33725  esplymhp  33726  esplyfv1  33727  esplyfv  33728  esplyfval3  33730  constrsuc  33895  locfinreflem  33997  zarclsiin  34028  zarcls  34031  zartopn  34032  esumrnmpt2  34225  esumpinfval  34230  sigagensiga  34298  ldgenpisyslem1  34320  ldgenpisys  34323  measvuni  34371  imambfm  34419  dya2iocuni  34440  omscl  34452  oms0  34454  omsmon  34455  omssubadd  34457  carsgcl  34461  oddpwdc  34511  eulerpartlem1  34524  eulerpartlemt  34528  eulerpartgbij  34529  eulerpartlemmf  34532  eulerpartlemgh  34535  eulerpartlemgs2  34537  ballotlem2  34646  ballotlemfc0  34650  ballotlemfcc  34651  ballotlemfmpn  34652  ballotlemiex  34659  ballotlemsup  34662  ballotlem7  34693  ballotth  34695  reprpmtf1o  34783  breprexplema  34787  hgt750lema  34814  bnj110  35014  bnj1204  35168  bnj1311  35180  fnrelpredd  35247  subfacp1lem6  35379  erdszelem2  35386  connpconn  35429  cvmliftmolem2  35476  cvmliftlem15  35492  cvmlift2lem12  35508  snmlff  35523  satfrnmapom  35564  rankeq1o  36365  finminlem  36512  fnessref  36551  neibastop1  36553  neibastop2lem  36554  weiunlem  36657  weiunse  36662  bj-rabtr  37131  bj-rabtrAUTO  37133  bj-vecssmod  37482  icoreresf  37553  phpreu  37801  fin2so  37804  poimirlem26  37843  poimirlem31  37848  poimirlem32  37849  opnmbllem0  37853  mblfinlem1  37854  mblfinlem2  37855  ismblfin  37858  mbfposadd  37864  cnambfre  37865  cover2  37912  indexa  37930  fdc  37942  sstotbnd2  37971  sstotbnd3  37973  igenidl  38260  prnc  38264  toycom  39229  lkrlss  39351  atlatmstc  39575  atlatle  39576  glbconN  39633  linepsubN  40008  pmapssat  40015  pmaple  40017  pmapsub  40024  paddssat  40070  diass  41298  diaglbN  41311  diaintclN  41314  diassdvaN  41316  docaclN  41380  dibglbN  41422  dibintclN  41423  diclspsn  41450  dihglblem2N  41550  dih1dimatlem  41585  dihglb2  41598  dochval2  41608  dochcl  41609  dochvalr  41613  doch2val2  41620  dochss  41621  dochocss  41622  lclkr  41789  lclkrs  41795  lcdvbase  41849  lcdvbasess  41850  mapdunirnN  41906  aks4d1p4  42329  aks4d1p5  42330  aks4d1p7  42333  aks4d1p8  42337  sticksstones1  42396  aks6d1c6lem2  42421  grpods  42444  unitscyglem1  42445  unitscyglem2  42446  unitscyglem4  42448  mhpind  42833  mhphf  42836  prjcrv0  42872  infdesc  42882  mzpindd  42984  fiphp3d  43057  rencldnfilem  43058  irrapx1  43066  pellexlem3  43069  pellfundre  43119  pellfundge  43120  pellfundlb  43122  pellfundglb  43123  jm2.22  43233  jm2.23  43234  rpnnen3  43270  pwssplit4  43327  pwfi2f1o  43334  hbtlem6  43367  dgraalem  43383  dgraaub  43386  itgocn  43402  onintunirab  43465  nadd2rabord  43623  nadd1rabord  43627  rfovcnvf1od  44241  fsovfd  44249  fsovcnvlem  44250  binomcxplemdvbinom  44590  binomcxplemcvg  44591  binomcxplemnotnn0  44593  uzwo4  45294  disjf1o  45431  icof  45459  allbutfiinf  45660  supminfxr  45704  supminfxr2  45709  fsumsupp0  45820  sumnnodd  45872  fnlimabslt  45919  liminfvalxr  46023  ioodvbdlimc1lem1  46171  dvnprodlem1  46186  dvnprodlem2  46187  stoweidlem14  46254  stoweidlem34  46274  stoweidlem44  46284  stoweidlem50  46290  stoweidlem51  46291  stoweidlem52  46292  stoweidlem57  46297  stoweidlem59  46299  fourierdlem19  46366  fourierdlem20  46367  fourierdlem25  46372  fourierdlem31  46378  fourierdlem37  46384  fourierdlem42  46389  fourierdlem51  46397  fourierdlem54  46400  fourierdlem64  46410  fourierdlem79  46425  elaa2lem  46473  etransclem16  46490  etransclem24  46498  etransclem31  46505  etransclem33  46507  etransclem34  46508  etransclem48  46522  salgencl  46572  salexct  46574  salgenuni  46577  subsaliuncllem  46597  meadjiunlem  46705  caragenss  46744  caratheodory  46768  ovnlecvr  46798  ovnlerp  46802  ovn0lem  46805  ovnsubaddlem1  46810  hoidmv1lelem1  46831  hoidmv1lelem3  46833  hoidmvlelem1  46835  hoidmvlelem2  46836  hoidmvlelem3  46837  hoidmvlelem4  46838  ovnhoilem1  46841  ovnhoilem2  46842  ovnlecvr2  46850  ovncvr2  46851  opnvonmbllem2  46873  ovolval4lem1  46889  pimconstlt1  46942  pimgtmnf2  46954  pimdecfgtioc  46955  pimincfltioc  46956  pimdecfgtioo  46957  pimincfltioo  46958  sssmf  46978  incsmflem  46981  smfaddlem1  47003  smfaddlem2  47004  decsmflem  47006  smflimlem1  47011  smflimlem2  47012  smflimlem3  47013  smfrec  47029  smfmullem4  47034  smfdiv  47037  smfsuplem1  47051  smfsuplem3  47053  smfinflem  47057  smflimsuplem1  47060  smflimsuplem7  47066  smfliminflem  47070  sprsymrelfolem1  47734  prmdvdsfmtnof1lem1  47826  prmdvdsfmtnof  47828  perfectALTVlem2  47964  isubgredg  48108  isubgruhgr  48110  isubgrgrim  48171  uhgrimisgrgric  48173  uspgrlimlem1  48230  uspgrlimlem4  48233  uspgrlim  48234  grlimgrtrilem2  48244  oddibas  48415  2zlidl  48482  2zrngbas  48484  2zrng0  48486  isclatd  49224  topclat  49239