Theorem ssrab2 4020

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

Syntax hints:  {crab 3389   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-ss 3906

This theorem is referenced by:  ssrab3  4022  ssrabeq  4024  iinrab2  5012  riinrab  5026  rabelpw  5277  rabexgOLD  5279  frminex  5610  wereu2  5628  predres  6303  frpomin  6304  frpoinsg  6307  ssimaex  6925  f1oresrab  7080  weniso  7309  canth  7321  riotacl  7341  riotassuni  7364  onminesb  7747  onminsb  7748  onintrab  7750  onnminsb  7753  onminex  7756  tfisg  7805  tfis  7806  suppssdm  8127  fnsuppres  8141  oeeulem  8537  nnawordex  8573  pmvalg  8784  fineqvlem  9176  ordtypelem3  9435  ordtypelem4  9436  ordtypelem6  9438  hartogs  9459  card2on  9469  wdom2d  9495  oemapvali  9605  frinsg  9675  tz9.12lem1  9711  tz9.12lem3  9713  rankf  9718  cardf2  9867  cardid2  9877  cardmin2  9923  acni3  9969  dfac2a  10052  cofsmo  10191  coftr  10195  fin2i2  10240  isfin2-2  10241  enfin2i  10243  fin1a2lem11  10332  fin1a2lem12  10333  axdc3lem4  10375  ac6  10402  ondomon  10485  alephval2  10495  pwfseqlem1  10581  pwfseqlem3  10583  wunccl  10667  tskmcl  10764  infm3  12115  uzf  12791  nnwos  12865  supminf  12885  zsupss  12887  rpnnen1lem1  12928  rpnnen1lem3  12929  rpnnen1lem5  12931  ixxf  13308  fzf  13465  flval3  13774  rabssnn0fi  13948  expge0  14060  expge1  14061  hashbclem  14414  01sqrexlem3  15206  rlimrege0  15541  incexc2  15803  bitsf  16396  bitsfzolem  16403  sadadd2lem  16428  sadadd3  16430  sadcl  16431  smupf  16447  smuval2  16451  smupvallem  16452  smucl  16453  smueqlem  16459  lcmcllem  16565  lcmn0cl  16566  lcmledvds  16568  lcmfval  16590  lcmfcllem  16594  lcmfn0cl  16595  lcmfledvds  16601  phicl2  16738  phibnd  16741  hashdvds  16745  phiprmpw  16746  phimullem  16749  eulerth  16753  phisum  16761  odzcllem  16763  odzdvds  16766  prmreclem1  16887  prmreclem2  16888  prmreclem3  16889  prmreclem4  16890  prmreclem5  16891  hashbccl  16974  prmgaplem3  17024  prmgaplem4  17025  prdsds  17427  mrcflem  17572  isacs1i  17623  wunnat  17926  dmcoass  18033  lublecl  18325  lubid  18326  rabsubmgmd  18672  mgmhmeql  18684  issubmd  18774  mhmeql  18794  cntzval  19296  cntzssv  19303  symgsssg  19442  symgfisg  19443  pmtrdifellem4  19454  odfval  19507  odlem1  19510  odlem2  19514  odngen  19552  gexlem1  19554  gexlem2  19557  sylow2alem2  19593  sylow2blem3  19597  oddvdssubg  19830  cyggex2  19872  ablfaclem3  20064  rgspncl  20590  lssacs  20962  lspf  20969  ocvfval  21646  ocvval  21647  dsmmval2  21716  dsmmsubg  21723  asplss  21853  aspsubrg  21855  psrass1lem  21912  psrdi  21943  psrdir  21944  psrass23l  21945  psrass23  21947  resspsrmul  21954  mplbas  21968  mplsubglem  21977  mplsubrglem  21982  mplmonmul  22014  psropprmul  22201  scmatlss  22490  smadiadet  22635  pmatcoe1fsupp  22666  cpmatsubgpmat  22685  fctop  22969  cctop  22971  ppttop  22972  epttop  22974  clscld  23012  neips  23078  neiptopnei  23097  ordtbaslem  23153  ordtuni  23155  ordtcld1  23162  ordtcld2  23163  cnpfval  23199  iscnp2  23204  cmpcov2  23355  cmpsublem  23364  tgcmp  23366  conncompcld  23399  1stcfb  23410  2ndc1stc  23416  2ndcdisj  23421  finlocfin  23485  kgentopon  23503  xkotf  23550  txkgen  23617  xkococnlem  23624  imastopn  23685  kqffn  23690  opnfbas  23807  flimfnfcls  23993  alexsubALT  24016  ptcmplem2  24018  symgtgp  24071  tgpconncompeqg  24077  tgpconncomp  24078  ghmcnp  24080  tsmsfbas  24093  eltsms  24098  utoptop  24199  utopbas  24200  blfvalps  24348  blfps  24371  blf  24372  nmoffn  24676  nmofval  24679  nmogelb  24681  nmolb  24682  nmof  24684  ishtpy  24939  clsocv  25217  rrxnm  25358  rrxbasefi  25377  minveclem3b  25395  minveclem4  25399  ovolcl  25445  ovollb  25446  ovolgelb  25447  ovolge0  25448  ovolshftlem1  25476  ovolshft  25478  ovolscalem1  25480  ovolscalem2  25481  ovolsca  25482  ovolicc2lem3  25486  shftmbl  25505  iundisj  25515  dyadmax  25565  dyadmbllem  25566  opnmbllem  25568  mdegmullem  26043  uc1pval  26105  mon1pval  26107  elqaalem1  26285  elqaalem3  26287  aannenlem2  26295  aalioulem2  26299  radcnvcl  26382  radcnvlt1  26383  radcnvle  26385  ftalem4  27039  ftalem5  27040  efnnfsumcl  27066  isppw  27077  sgmval2  27106  efchtdvds  27122  sqff1o  27145  fsumdvdsdiaglem  27146  fsumdvdsdiag  27147  fsumdvdscom  27148  musum  27154  muinv  27156  sgmmul  27164  ppiub  27167  vmasum  27179  logfac2  27180  perfectlem2  27193  lgsfcl  27268  lgscl  27274  lgsquadlem1  27343  lgsquadlem2  27344  rpvmasumlem  27450  mudivsum  27493  mulogsum  27495  mulog2sumlem2  27498  vmalogdivsum2  27501  logsqvma  27505  logsqvma2  27506  selberglem3  27510  selberg  27511  selberg34r  27534  pntsval2  27539  pntrlog2bndlem1  27540  ltsval2  27620  conway  27771  eqcuts2  27778  cutsun12  27782  cutbdaybnd  27787  cutbdaybnd2  27788  cutbdaylt  27790  bday1  27806  cuteq0  27807  madef  27828  leftssold  27863  rightssold  27864  madebdaylemlrcut  27891  sltsbday  27909  cofcut1  27912  cofcutr  27916  cutlt  27924  precsexlem8  28206  precsexlem11  28209  onssno  28246  oncutlt  28256  oniso  28263  bdayons  28268  bdayn0p1  28361  tglnunirn  28616  tglnssp  28620  incistruhgr  29148  upgrss  29157  upgrn0  29158  upgruhgr  29171  usgrss  29243  uspgrushgr  29246  ushgredgedg  29298  ushgredgedgloop  29300  vtxdun  29550  vtxdginducedm1  29612  wlknwwlksnbij  29956  hashwwlksnext  29982  frcond3  30339  numclwlk1lem2  30440  ocsh  31354  spancl  31407  shsval2i  31458  ococin  31479  chsupid  31483  speccl  31970  hatomistici  32433  chpssati  32434  iundisjf  32659  aciunf1  32736  fpwrelmap  32806  iundisjfi  32869  pwrssmgc  33060  cycpmco2f1  33185  cycpmco2rn  33186  cycpmco2lem1  33187  cycpmco2lem2  33188  cycpmco2lem3  33189  cycpmco2lem4  33190  cycpmco2lem5  33191  cycpmco2lem6  33192  cycpmco2lem7  33193  cycpmco2  33194  fxpss  33227  nsgmgclem  33471  extvfvcl  33680  mplmulmvr  33683  evlextv  33686  mplvrpmlem  33687  mplvrpmga  33689  mplvrpmrhm  33691  psrmonmul  33694  esplylem  33710  esplympl  33711  esplymhp  33712  esplyfv1  33713  esplyfv  33714  esplyfval3  33716  esplyfval1  33717  esplyfvaln  33718  constrsuc  33882  locfinreflem  33984  zarclsiin  34015  zarcls  34018  zartopn  34019  esumrnmpt2  34212  esumpinfval  34217  sigagensiga  34285  ldgenpisyslem1  34307  ldgenpisys  34310  measvuni  34358  imambfm  34406  dya2iocuni  34427  omscl  34439  oms0  34441  omsmon  34442  omssubadd  34444  carsgcl  34448  oddpwdc  34498  eulerpartlem1  34511  eulerpartlemt  34515  eulerpartgbij  34516  eulerpartlemmf  34519  eulerpartlemgh  34522  eulerpartlemgs2  34524  ballotlem2  34633  ballotlemfc0  34637  ballotlemfcc  34638  ballotlemfmpn  34639  ballotlemiex  34646  ballotlemsup  34649  ballotlem7  34680  ballotth  34682  reprpmtf1o  34770  breprexplema  34774  hgt750lema  34801  bnj110  35000  bnj1204  35154  bnj1311  35166  fnrelpredd  35234  subfacp1lem6  35367  erdszelem2  35374  connpconn  35417  cvmliftmolem2  35464  cvmliftlem15  35480  cvmlift2lem12  35496  snmlff  35511  satfrnmapom  35552  rankeq1o  36353  finminlem  36500  fnessref  36539  neibastop1  36541  neibastop2lem  36542  weiunlem  36645  weiunse  36650  bj-rabtr  37237  bj-rabtrAUTO  37239  bj-vecssmod  37595  icoreresf  37668  phpreu  37925  fin2so  37928  poimirlem26  37967  poimirlem31  37972  poimirlem32  37973  opnmbllem0  37977  mblfinlem1  37978  mblfinlem2  37979  ismblfin  37982  mbfposadd  37988  cnambfre  37989  cover2  38036  indexa  38054  fdc  38066  sstotbnd2  38095  sstotbnd3  38097  igenidl  38384  prnc  38388  toycom  39419  lkrlss  39541  atlatmstc  39765  atlatle  39766  glbconN  39823  linepsubN  40198  pmapssat  40205  pmaple  40207  pmapsub  40214  paddssat  40260  diass  41488  diaglbN  41501  diaintclN  41504  diassdvaN  41506  docaclN  41570  dibglbN  41612  dibintclN  41613  diclspsn  41640  dihglblem2N  41740  dih1dimatlem  41775  dihglb2  41788  dochval2  41798  dochcl  41799  dochvalr  41803  doch2val2  41810  dochss  41811  dochocss  41812  lclkr  41979  lclkrs  41985  lcdvbase  42039  lcdvbasess  42040  mapdunirnN  42096  aks4d1p4  42518  aks4d1p5  42519  aks4d1p7  42522  aks4d1p8  42526  sticksstones1  42585  aks6d1c6lem2  42610  grpods  42633  unitscyglem1  42634  unitscyglem2  42635  unitscyglem4  42637  mhpind  43027  mhphf  43030  prjcrv0  43066  infdesc  43076  mzpindd  43178  fiphp3d  43247  rencldnfilem  43248  irrapx1  43256  pellexlem3  43259  pellfundre  43309  pellfundge  43310  pellfundlb  43312  pellfundglb  43313  jm2.22  43423  jm2.23  43424  rpnnen3  43460  pwssplit4  43517  pwfi2f1o  43524  hbtlem6  43557  dgraalem  43573  dgraaub  43576  itgocn  43592  onintunirab  43655  nadd2rabord  43813  nadd1rabord  43817  rfovcnvf1od  44431  fsovfd  44439  fsovcnvlem  44440  binomcxplemdvbinom  44780  binomcxplemcvg  44781  binomcxplemnotnn0  44783  uzwo4  45484  disjf1o  45621  icof  45648  allbutfiinf  45848  supminfxr  45892  supminfxr2  45897  fsumsupp0  46008  sumnnodd  46060  fnlimabslt  46107  liminfvalxr  46211  ioodvbdlimc1lem1  46359  dvnprodlem1  46374  dvnprodlem2  46375  stoweidlem14  46442  stoweidlem34  46462  stoweidlem44  46472  stoweidlem50  46478  stoweidlem51  46479  stoweidlem52  46480  stoweidlem57  46485  stoweidlem59  46487  fourierdlem19  46554  fourierdlem20  46555  fourierdlem25  46560  fourierdlem31  46566  fourierdlem37  46572  fourierdlem42  46577  fourierdlem51  46585  fourierdlem54  46588  fourierdlem64  46598  fourierdlem79  46613  elaa2lem  46661  etransclem16  46678  etransclem24  46686  etransclem31  46693  etransclem33  46695  etransclem34  46696  etransclem48  46710  salgencl  46760  salexct  46762  salgenuni  46765  subsaliuncllem  46785  meadjiunlem  46893  caragenss  46932  caratheodory  46956  ovnlecvr  46986  ovnlerp  46990  ovn0lem  46993  ovnsubaddlem1  46998  hoidmv1lelem1  47019  hoidmv1lelem3  47021  hoidmvlelem1  47023  hoidmvlelem2  47024  hoidmvlelem3  47025  hoidmvlelem4  47026  ovnhoilem1  47029  ovnhoilem2  47030  ovnlecvr2  47038  ovncvr2  47039  opnvonmbllem2  47061  ovolval4lem1  47077  pimconstlt1  47130  pimgtmnf2  47142  pimdecfgtioc  47143  pimincfltioc  47144  pimdecfgtioo  47145  pimincfltioo  47146  sssmf  47166  incsmflem  47169  smfaddlem1  47191  smfaddlem2  47192  decsmflem  47194  smflimlem1  47199  smflimlem2  47200  smflimlem3  47201  smfrec  47217  smfmullem4  47222  smfdiv  47225  smfsuplem1  47239  smfsuplem3  47241  smfinflem  47245  smflimsuplem1  47248  smflimsuplem7  47254  smfliminflem  47258  sprsymrelfolem1  47952  prmdvdsfmtnof1lem1  48047  prmdvdsfmtnof  48049  perfectALTVlem2  48198  isubgredg  48342  isubgruhgr  48344  isubgrgrim  48405  uhgrimisgrgric  48407  uspgrlimlem1  48464  uspgrlimlem4  48467  uspgrlim  48468  grlimgrtrilem2  48478  oddibas  48649  2zlidl  48716  2zrngbas  48718  2zrng0  48720  isclatd  49458  topclat  49473