Theorem ssrab2 4078

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

Syntax hints:  {crab 3433   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  ssrab3  4081  ssrabeq  4083  iinrab2  5074  riinrab  5088  rabexg  5332  pwnss  5350  rabelpw  5353  frminex  5657  wereu2  5674  predres  6341  frpomin  6342  frpoinsg  6345  wfisgOLD  6356  ssimaex  6977  f1oresrab  7125  weniso  7351  canth  7362  riotacl  7383  riotassuni  7406  onminesb  7781  onminsb  7782  onintrab  7784  onnminsb  7787  onminex  7790  tfisg  7843  tfis  7844  suppssdm  8162  fnsuppres  8176  oeeulem  8601  nnawordex  8637  pmvalg  8831  fineqvlem  9262  ordtypelem3  9515  ordtypelem4  9516  ordtypelem6  9518  hartogs  9539  card2on  9549  wdom2d  9575  oemapvali  9679  frinsg  9746  tz9.12lem1  9782  tz9.12lem3  9784  rankf  9789  cardf2  9938  cardid2  9948  cardmin2  9994  acni3  10042  dfac2a  10124  cofsmo  10264  coftr  10268  fin2i2  10313  isfin2-2  10314  enfin2i  10316  fin1a2lem11  10405  fin1a2lem12  10406  axdc3lem4  10448  ac6  10475  ondomon  10558  alephval2  10567  pwfseqlem1  10653  pwfseqlem3  10655  wunccl  10739  tskmcl  10836  infm3  12173  uzf  12825  nnwos  12899  supminf  12919  zsupss  12921  rpnnen1lem1  12962  rpnnen1lem3  12963  rpnnen1lem5  12965  ixxf  13334  fzf  13488  flval3  13780  rabssnn0fi  13951  expge0  14064  expge1  14065  hashbclem  14411  01sqrexlem3  15191  rlimrege0  15523  incexc2  15784  bitsf  16368  bitsfzolem  16375  sadadd2lem  16400  sadadd3  16402  sadcl  16403  smupf  16419  smuval2  16423  smupvallem  16424  smucl  16425  smueqlem  16431  lcmcllem  16533  lcmn0cl  16534  lcmledvds  16536  lcmfval  16558  lcmfcllem  16562  lcmfn0cl  16563  lcmfledvds  16569  phicl2  16701  phibnd  16704  hashdvds  16708  phiprmpw  16709  phimullem  16712  eulerth  16716  phisum  16723  odzcllem  16725  odzdvds  16728  prmreclem1  16849  prmreclem2  16850  prmreclem3  16851  prmreclem4  16852  prmreclem5  16853  hashbccl  16936  prmgaplem3  16986  prmgaplem4  16987  prdsds  17410  mrcflem  17550  isacs1i  17601  wunnat  17907  wunnatOLD  17908  dmcoass  18016  lublecl  18314  lubid  18315  issubmd  18687  mhmeql  18707  cntzval  19185  cntzssv  19192  symgsssg  19335  symgfisg  19336  pmtrdifellem4  19347  odfval  19400  odlem1  19403  odlem2  19407  odngen  19445  gexlem1  19447  gexlem2  19450  sylow2alem2  19486  sylow2blem3  19490  oddvdssubg  19723  cyggex2  19765  ablfaclem3  19957  lssacs  20578  lspf  20585  ocvfval  21219  ocvval  21220  dsmmval2  21291  dsmmsubg  21298  asplss  21428  aspsubrg  21430  psrass1lemOLD  21493  psrass1lem  21496  psrdi  21526  psrdir  21527  psrass23l  21528  psrass23  21530  resspsrmul  21537  mplbas  21549  mplsubglem  21558  mplsubrglem  21563  mplmonmul  21591  psropprmul  21760  scmatlss  22027  smadiadet  22172  pmatcoe1fsupp  22203  cpmatsubgpmat  22222  fctop  22507  cctop  22509  ppttop  22510  epttop  22512  clscld  22551  neips  22617  neiptopnei  22636  ordtbaslem  22692  ordtuni  22694  ordtcld1  22701  ordtcld2  22702  cnpfval  22738  iscnp2  22743  cmpcov2  22894  cmpsublem  22903  tgcmp  22905  conncompcld  22938  1stcfb  22949  2ndc1stc  22955  2ndcdisj  22960  finlocfin  23024  kgentopon  23042  xkotf  23089  txkgen  23156  xkococnlem  23163  imastopn  23224  kqffn  23229  opnfbas  23346  flimfnfcls  23532  alexsubALT  23555  ptcmplem2  23557  symgtgp  23610  tgpconncompeqg  23616  tgpconncomp  23617  ghmcnp  23619  tsmsfbas  23632  eltsms  23637  utoptop  23739  utopbas  23740  blfvalps  23889  blfps  23912  blf  23913  nmoffn  24228  nmofval  24231  nmogelb  24233  nmolb  24234  nmof  24236  ishtpy  24488  clsocv  24767  rrxnm  24908  rrxbasefi  24927  minveclem3b  24945  minveclem4  24949  ovolcl  24995  ovollb  24996  ovolgelb  24997  ovolge0  24998  ovolshftlem1  25026  ovolshft  25028  ovolscalem1  25030  ovolscalem2  25031  ovolsca  25032  ovolicc2lem3  25036  shftmbl  25055  iundisj  25065  dyadmax  25115  dyadmbllem  25116  opnmbllem  25118  mdegmullem  25596  uc1pval  25657  mon1pval  25659  elqaalem1  25832  elqaalem3  25834  aannenlem2  25842  aalioulem2  25846  radcnvcl  25929  radcnvlt1  25930  radcnvle  25932  ftalem4  26580  ftalem5  26581  efnnfsumcl  26607  isppw  26618  sgmval2  26647  efchtdvds  26663  sqff1o  26686  fsumdvdsdiaglem  26687  fsumdvdsdiag  26688  fsumdvdscom  26689  musum  26695  muinv  26697  sgmmul  26704  ppiub  26707  vmasum  26719  logfac2  26720  perfectlem2  26733  lgsfcl  26808  lgscl  26814  lgsquadlem1  26883  lgsquadlem2  26884  rpvmasumlem  26990  mudivsum  27033  mulogsum  27035  mulog2sumlem2  27038  vmalogdivsum2  27041  logsqvma  27045  logsqvma2  27046  selberglem3  27050  selberg  27051  selberg34r  27074  pntsval2  27079  pntrlog2bndlem1  27080  sltval2  27159  conway  27300  eqscut2  27307  scutun12  27311  scutbdaybnd  27316  scutbdaybnd2  27317  scutbdaylt  27319  bday1s  27332  cuteq0  27333  madef  27351  leftssold  27373  rightssold  27374  madebdaylemlrcut  27393  cofcut1  27407  cofcutr  27411  cutlt  27419  precsexlem8  27660  precsexlem11  27663  tglnunirn  27799  tglnssp  27803  incistruhgr  28339  upgrss  28348  upgrn0  28349  upgruhgr  28362  usgrss  28434  uspgrushgr  28435  ushgredgedg  28486  ushgredgedgloop  28488  vtxdun  28738  vtxdginducedm1  28800  wlknwwlksnbij  29142  hashwwlksnext  29168  frcond3  29522  numclwlk1lem2  29623  ocsh  30536  spancl  30589  shsval2i  30640  ococin  30661  chsupid  30665  speccl  31152  hatomistici  31615  chpssati  31616  iundisjf  31820  aciunf1  31888  fpwrelmap  31958  iundisjfi  32007  pwrssmgc  32170  cycpmco2f1  32283  cycpmco2rn  32284  cycpmco2lem1  32285  cycpmco2lem2  32286  cycpmco2lem3  32287  cycpmco2lem4  32288  cycpmco2lem5  32289  cycpmco2lem6  32290  cycpmco2lem7  32291  cycpmco2  32292  nsgmgclem  32522  locfinreflem  32820  zarclsiin  32851  zarcls  32854  zartopn  32855  esumrnmpt2  33066  esumpinfval  33071  sigagensiga  33139  ldgenpisyslem1  33161  ldgenpisys  33164  measvuni  33212  imambfm  33261  dya2iocuni  33282  omscl  33294  oms0  33296  omsmon  33297  omssubadd  33299  carsgcl  33303  oddpwdc  33353  eulerpartlem1  33366  eulerpartlemt  33370  eulerpartgbij  33371  eulerpartlemmf  33374  eulerpartlemgh  33377  eulerpartlemgs2  33379  ballotlem2  33487  ballotlemfc0  33491  ballotlemfcc  33492  ballotlemfmpn  33493  ballotlemiex  33500  ballotlemsup  33503  ballotlem7  33534  ballotth  33536  reprpmtf1o  33638  breprexplema  33642  hgt750lema  33669  bnj110  33869  bnj1204  34023  bnj1311  34035  fnrelpredd  34092  subfacp1lem6  34176  erdszelem2  34183  connpconn  34226  cvmliftmolem2  34273  cvmliftlem15  34289  cvmlift2lem12  34305  snmlff  34320  satfrnmapom  34361  rankeq1o  35143  finminlem  35203  fnessref  35242  neibastop1  35244  neibastop2lem  35245  bj-rabtr  35810  bj-rabtrAUTO  35812  bj-vecssmod  36162  icoreresf  36233  phpreu  36472  fin2so  36475  poimirlem26  36514  poimirlem31  36519  poimirlem32  36520  opnmbllem0  36524  mblfinlem1  36525  mblfinlem2  36526  ismblfin  36529  mbfposadd  36535  cnambfre  36536  cover2  36583  indexa  36601  fdc  36613  sstotbnd2  36642  sstotbnd3  36644  igenidl  36931  prnc  36935  toycom  37843  lkrlss  37965  atlatmstc  38189  atlatle  38190  glbconN  38247  glbconNOLD  38248  linepsubN  38623  pmapssat  38630  pmaple  38632  pmapsub  38639  paddssat  38685  diass  39913  diaglbN  39926  diaintclN  39929  diassdvaN  39931  docaclN  39995  dibglbN  40037  dibintclN  40038  diclspsn  40065  dihglblem2N  40165  dih1dimatlem  40200  dihglb2  40213  dochval2  40223  dochcl  40224  dochvalr  40228  doch2val2  40235  dochss  40236  dochocss  40237  lclkr  40404  lclkrs  40410  lcdvbase  40464  lcdvbasess  40465  mapdunirnN  40521  aks4d1p4  40944  aks4d1p5  40945  aks4d1p7  40948  aks4d1p8  40952  sticksstones1  40962  mhpind  41166  mhphf  41169  prjcrv0  41375  infdesc  41385  mzpindd  41484  fiphp3d  41557  rencldnfilem  41558  irrapx1  41566  pellexlem3  41569  pellfundre  41619  pellfundge  41620  pellfundlb  41622  pellfundglb  41623  jm2.22  41734  jm2.23  41735  rpnnen3  41771  pwssplit4  41831  pwfi2f1o  41838  hbtlem6  41871  dgraalem  41887  dgraaub  41890  itgocn  41906  rgspncl  41911  onintunirab  41976  nadd2rabord  42135  nadd1rabord  42139  rfovcnvf1od  42755  fsovfd  42763  fsovcnvlem  42764  binomcxplemdvbinom  43112  binomcxplemcvg  43113  binomcxplemnotnn0  43115  uzwo4  43740  disjf1o  43889  icof  43918  allbutfiinf  44130  supminfxr  44174  supminfxr2  44179  fsumsupp0  44294  sumnnodd  44346  fnlimabslt  44395  liminfvalxr  44499  ioodvbdlimc1lem1  44647  dvnprodlem1  44662  dvnprodlem2  44663  stoweidlem14  44730  stoweidlem34  44750  stoweidlem44  44760  stoweidlem50  44766  stoweidlem51  44767  stoweidlem52  44768  stoweidlem57  44773  stoweidlem59  44775  fourierdlem19  44842  fourierdlem20  44843  fourierdlem25  44848  fourierdlem31  44854  fourierdlem37  44860  fourierdlem42  44865  fourierdlem51  44873  fourierdlem54  44876  fourierdlem64  44886  fourierdlem79  44901  elaa2lem  44949  etransclem16  44966  etransclem24  44974  etransclem31  44981  etransclem33  44983  etransclem34  44984  etransclem48  44998  salgencl  45048  salexct  45050  salgenuni  45053  subsaliuncllem  45073  meadjiunlem  45181  caragenss  45220  caratheodory  45244  ovnlecvr  45274  ovnlerp  45278  ovn0lem  45281  ovnsubaddlem1  45286  hoidmv1lelem1  45307  hoidmv1lelem3  45309  hoidmvlelem1  45311  hoidmvlelem2  45312  hoidmvlelem3  45313  hoidmvlelem4  45314  ovnhoilem1  45317  ovnhoilem2  45318  ovnlecvr2  45326  ovncvr2  45327  opnvonmbllem2  45349  ovolval4lem1  45365  pimconstlt1  45418  pimiooltgt  45426  pimgtmnf2  45430  pimdecfgtioc  45431  pimincfltioc  45432  pimdecfgtioo  45433  pimincfltioo  45434  sssmf  45454  incsmflem  45457  smfaddlem1  45479  smfaddlem2  45480  decsmflem  45482  smflimlem1  45487  smflimlem2  45488  smflimlem3  45489  smfrec  45505  smfmullem4  45510  smfdiv  45513  smfsuplem1  45527  smfsuplem3  45529  smfinflem  45533  smflimsuplem1  45536  smflimsuplem7  45542  smfliminflem  45546  sprsymrelfolem1  46160  prmdvdsfmtnof1lem1  46252  prmdvdsfmtnof  46254  perfectALTVlem2  46390  rabsubmgmd  46561  mgmhmeql  46573  oddibas  46583  2zlidl  46832  2zrngbas  46834  2zrng0  46836  isclatd  47608  topclat  47623