Theorem ssrab2 4080

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

Syntax hints:  {crab 3436   ⊆ wss 3951

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-ss 3968

This theorem is referenced by:  ssrab3  4082  ssrabeq  4084  iinrab2  5070  riinrab  5084  rabelpw  5336  rabexgOLD  5338  frminex  5664  wereu2  5682  predres  6360  frpomin  6361  frpoinsg  6364  wfisgOLD  6375  ssimaex  6994  f1oresrab  7147  weniso  7374  canth  7385  riotacl  7405  riotassuni  7428  onminesb  7813  onminsb  7814  onintrab  7816  onnminsb  7819  onminex  7822  tfisg  7875  tfis  7876  suppssdm  8202  fnsuppres  8216  oeeulem  8639  nnawordex  8675  pmvalg  8877  fineqvlem  9298  ordtypelem3  9560  ordtypelem4  9561  ordtypelem6  9563  hartogs  9584  card2on  9594  wdom2d  9620  oemapvali  9724  frinsg  9791  tz9.12lem1  9827  tz9.12lem3  9829  rankf  9834  cardf2  9983  cardid2  9993  cardmin2  10039  acni3  10087  dfac2a  10170  cofsmo  10309  coftr  10313  fin2i2  10358  isfin2-2  10359  enfin2i  10361  fin1a2lem11  10450  fin1a2lem12  10451  axdc3lem4  10493  ac6  10520  ondomon  10603  alephval2  10612  pwfseqlem1  10698  pwfseqlem3  10700  wunccl  10784  tskmcl  10881  infm3  12227  uzf  12881  nnwos  12957  supminf  12977  zsupss  12979  rpnnen1lem1  13020  rpnnen1lem3  13021  rpnnen1lem5  13023  ixxf  13397  fzf  13551  flval3  13855  rabssnn0fi  14027  expge0  14139  expge1  14140  hashbclem  14491  01sqrexlem3  15283  rlimrege0  15615  incexc2  15874  bitsf  16464  bitsfzolem  16471  sadadd2lem  16496  sadadd3  16498  sadcl  16499  smupf  16515  smuval2  16519  smupvallem  16520  smucl  16521  smueqlem  16527  lcmcllem  16633  lcmn0cl  16634  lcmledvds  16636  lcmfval  16658  lcmfcllem  16662  lcmfn0cl  16663  lcmfledvds  16669  phicl2  16805  phibnd  16808  hashdvds  16812  phiprmpw  16813  phimullem  16816  eulerth  16820  phisum  16828  odzcllem  16830  odzdvds  16833  prmreclem1  16954  prmreclem2  16955  prmreclem3  16956  prmreclem4  16957  prmreclem5  16958  hashbccl  17041  prmgaplem3  17091  prmgaplem4  17092  prdsds  17509  mrcflem  17649  isacs1i  17700  wunnat  18004  dmcoass  18111  lublecl  18406  lubid  18407  rabsubmgmd  18717  mgmhmeql  18729  issubmd  18819  mhmeql  18839  cntzval  19339  cntzssv  19346  symgsssg  19485  symgfisg  19486  pmtrdifellem4  19497  odfval  19550  odlem1  19553  odlem2  19557  odngen  19595  gexlem1  19597  gexlem2  19600  sylow2alem2  19636  sylow2blem3  19640  oddvdssubg  19873  cyggex2  19915  ablfaclem3  20107  rgspncl  20613  lssacs  20965  lspf  20972  ocvfval  21684  ocvval  21685  dsmmval2  21756  dsmmsubg  21763  asplss  21894  aspsubrg  21896  psrass1lem  21952  psrdi  21985  psrdir  21986  psrass23l  21987  psrass23  21989  resspsrmul  21996  mplbas  22010  mplsubglem  22019  mplsubrglem  22024  mplmonmul  22054  psropprmul  22239  scmatlss  22531  smadiadet  22676  pmatcoe1fsupp  22707  cpmatsubgpmat  22726  fctop  23011  cctop  23013  ppttop  23014  epttop  23016  clscld  23055  neips  23121  neiptopnei  23140  ordtbaslem  23196  ordtuni  23198  ordtcld1  23205  ordtcld2  23206  cnpfval  23242  iscnp2  23247  cmpcov2  23398  cmpsublem  23407  tgcmp  23409  conncompcld  23442  1stcfb  23453  2ndc1stc  23459  2ndcdisj  23464  finlocfin  23528  kgentopon  23546  xkotf  23593  txkgen  23660  xkococnlem  23667  imastopn  23728  kqffn  23733  opnfbas  23850  flimfnfcls  24036  alexsubALT  24059  ptcmplem2  24061  symgtgp  24114  tgpconncompeqg  24120  tgpconncomp  24121  ghmcnp  24123  tsmsfbas  24136  eltsms  24141  utoptop  24243  utopbas  24244  blfvalps  24393  blfps  24416  blf  24417  nmoffn  24732  nmofval  24735  nmogelb  24737  nmolb  24738  nmof  24740  ishtpy  25004  clsocv  25284  rrxnm  25425  rrxbasefi  25444  minveclem3b  25462  minveclem4  25466  ovolcl  25513  ovollb  25514  ovolgelb  25515  ovolge0  25516  ovolshftlem1  25544  ovolshft  25546  ovolscalem1  25548  ovolscalem2  25549  ovolsca  25550  ovolicc2lem3  25554  shftmbl  25573  iundisj  25583  dyadmax  25633  dyadmbllem  25634  opnmbllem  25636  mdegmullem  26117  uc1pval  26179  mon1pval  26181  elqaalem1  26361  elqaalem3  26363  aannenlem2  26371  aalioulem2  26375  radcnvcl  26460  radcnvlt1  26461  radcnvle  26463  ftalem4  27119  ftalem5  27120  efnnfsumcl  27146  isppw  27157  sgmval2  27186  efchtdvds  27202  sqff1o  27225  fsumdvdsdiaglem  27226  fsumdvdsdiag  27227  fsumdvdscom  27228  musum  27234  muinv  27236  sgmmul  27245  ppiub  27248  vmasum  27260  logfac2  27261  perfectlem2  27274  lgsfcl  27349  lgscl  27355  lgsquadlem1  27424  lgsquadlem2  27425  rpvmasumlem  27531  mudivsum  27574  mulogsum  27576  mulog2sumlem2  27579  vmalogdivsum2  27582  logsqvma  27586  logsqvma2  27587  selberglem3  27591  selberg  27592  selberg34r  27615  pntsval2  27620  pntrlog2bndlem1  27621  sltval2  27701  conway  27844  eqscut2  27851  scutun12  27855  scutbdaybnd  27860  scutbdaybnd2  27861  scutbdaylt  27863  bday1s  27876  cuteq0  27877  madef  27895  leftssold  27917  rightssold  27918  madebdaylemlrcut  27937  cofcut1  27954  cofcutr  27958  cutlt  27966  precsexlem8  28238  precsexlem11  28241  onssno  28277  tglnunirn  28556  tglnssp  28560  incistruhgr  29096  upgrss  29105  upgrn0  29106  upgruhgr  29119  usgrss  29191  uspgrushgr  29194  ushgredgedg  29246  ushgredgedgloop  29248  vtxdun  29499  vtxdginducedm1  29561  wlknwwlksnbij  29908  hashwwlksnext  29934  frcond3  30288  numclwlk1lem2  30389  ocsh  31302  spancl  31355  shsval2i  31406  ococin  31427  chsupid  31431  speccl  31918  hatomistici  32381  chpssati  32382  iundisjf  32602  aciunf1  32673  fpwrelmap  32744  iundisjfi  32798  pwrssmgc  32990  cycpmco2f1  33144  cycpmco2rn  33145  cycpmco2lem1  33146  cycpmco2lem2  33147  cycpmco2lem3  33148  cycpmco2lem4  33149  cycpmco2lem5  33150  cycpmco2lem6  33151  cycpmco2lem7  33152  cycpmco2  33153  nsgmgclem  33439  constrsuc  33779  locfinreflem  33839  zarclsiin  33870  zarcls  33873  zartopn  33874  esumrnmpt2  34069  esumpinfval  34074  sigagensiga  34142  ldgenpisyslem1  34164  ldgenpisys  34167  measvuni  34215  imambfm  34264  dya2iocuni  34285  omscl  34297  oms0  34299  omsmon  34300  omssubadd  34302  carsgcl  34306  oddpwdc  34356  eulerpartlem1  34369  eulerpartlemt  34373  eulerpartgbij  34374  eulerpartlemmf  34377  eulerpartlemgh  34380  eulerpartlemgs2  34382  ballotlem2  34491  ballotlemfc0  34495  ballotlemfcc  34496  ballotlemfmpn  34497  ballotlemiex  34504  ballotlemsup  34507  ballotlem7  34538  ballotth  34540  reprpmtf1o  34641  breprexplema  34645  hgt750lema  34672  bnj110  34872  bnj1204  35026  bnj1311  35038  fnrelpredd  35103  subfacp1lem6  35190  erdszelem2  35197  connpconn  35240  cvmliftmolem2  35287  cvmliftlem15  35303  cvmlift2lem12  35319  snmlff  35334  satfrnmapom  35375  rankeq1o  36172  finminlem  36319  fnessref  36358  neibastop1  36360  neibastop2lem  36361  weiunlem2  36464  weiunse  36469  bj-rabtr  36931  bj-rabtrAUTO  36933  bj-vecssmod  37282  icoreresf  37353  phpreu  37611  fin2so  37614  poimirlem26  37653  poimirlem31  37658  poimirlem32  37659  opnmbllem0  37663  mblfinlem1  37664  mblfinlem2  37665  ismblfin  37668  mbfposadd  37674  cnambfre  37675  cover2  37722  indexa  37740  fdc  37752  sstotbnd2  37781  sstotbnd3  37783  igenidl  38070  prnc  38074  toycom  38974  lkrlss  39096  atlatmstc  39320  atlatle  39321  glbconN  39378  glbconNOLD  39379  linepsubN  39754  pmapssat  39761  pmaple  39763  pmapsub  39770  paddssat  39816  diass  41044  diaglbN  41057  diaintclN  41060  diassdvaN  41062  docaclN  41126  dibglbN  41168  dibintclN  41169  diclspsn  41196  dihglblem2N  41296  dih1dimatlem  41331  dihglb2  41344  dochval2  41354  dochcl  41355  dochvalr  41359  doch2val2  41366  dochss  41367  dochocss  41368  lclkr  41535  lclkrs  41541  lcdvbase  41595  lcdvbasess  41596  mapdunirnN  41652  aks4d1p4  42080  aks4d1p5  42081  aks4d1p7  42084  aks4d1p8  42088  sticksstones1  42147  aks6d1c6lem2  42172  grpods  42195  unitscyglem1  42196  unitscyglem2  42197  unitscyglem4  42199  mhpind  42604  mhphf  42607  prjcrv0  42643  infdesc  42653  mzpindd  42757  fiphp3d  42830  rencldnfilem  42831  irrapx1  42839  pellexlem3  42842  pellfundre  42892  pellfundge  42893  pellfundlb  42895  pellfundglb  42896  jm2.22  43007  jm2.23  43008  rpnnen3  43044  pwssplit4  43101  pwfi2f1o  43108  hbtlem6  43141  dgraalem  43157  dgraaub  43160  itgocn  43176  onintunirab  43239  nadd2rabord  43398  nadd1rabord  43402  rfovcnvf1od  44017  fsovfd  44025  fsovcnvlem  44026  binomcxplemdvbinom  44372  binomcxplemcvg  44373  binomcxplemnotnn0  44375  uzwo4  45058  disjf1o  45196  icof  45224  allbutfiinf  45431  supminfxr  45475  supminfxr2  45480  fsumsupp0  45593  sumnnodd  45645  fnlimabslt  45694  liminfvalxr  45798  ioodvbdlimc1lem1  45946  dvnprodlem1  45961  dvnprodlem2  45962  stoweidlem14  46029  stoweidlem34  46049  stoweidlem44  46059  stoweidlem50  46065  stoweidlem51  46066  stoweidlem52  46067  stoweidlem57  46072  stoweidlem59  46074  fourierdlem19  46141  fourierdlem20  46142  fourierdlem25  46147  fourierdlem31  46153  fourierdlem37  46159  fourierdlem42  46164  fourierdlem51  46172  fourierdlem54  46175  fourierdlem64  46185  fourierdlem79  46200  elaa2lem  46248  etransclem16  46265  etransclem24  46273  etransclem31  46280  etransclem33  46282  etransclem34  46283  etransclem48  46297  salgencl  46347  salexct  46349  salgenuni  46352  subsaliuncllem  46372  meadjiunlem  46480  caragenss  46519  caratheodory  46543  ovnlecvr  46573  ovnlerp  46577  ovn0lem  46580  ovnsubaddlem1  46585  hoidmv1lelem1  46606  hoidmv1lelem3  46608  hoidmvlelem1  46610  hoidmvlelem2  46611  hoidmvlelem3  46612  hoidmvlelem4  46613  ovnhoilem1  46616  ovnhoilem2  46617  ovnlecvr2  46625  ovncvr2  46626  opnvonmbllem2  46648  ovolval4lem1  46664  pimconstlt1  46717  pimiooltgt  46725  pimgtmnf2  46729  pimdecfgtioc  46730  pimincfltioc  46731  pimdecfgtioo  46732  pimincfltioo  46733  sssmf  46753  incsmflem  46756  smfaddlem1  46778  smfaddlem2  46779  decsmflem  46781  smflimlem1  46786  smflimlem2  46787  smflimlem3  46788  smfrec  46804  smfmullem4  46809  smfdiv  46812  smfsuplem1  46826  smfsuplem3  46828  smfinflem  46832  smflimsuplem1  46835  smflimsuplem7  46841  smfliminflem  46845  sprsymrelfolem1  47479  prmdvdsfmtnof1lem1  47571  prmdvdsfmtnof  47573  perfectALTVlem2  47709  isubgredg  47852  isubgruhgr  47854  isubgrgrim  47897  uhgrimisgrgric  47899  uspgrlimlem1  47955  uspgrlimlem4  47958  uspgrlim  47959  grlimgrtrilem2  47962  oddibas  48089  2zlidl  48156  2zrngbas  48158  2zrng0  48160  isclatd  48872  topclat  48887