Theorem ssrab2 4103

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

Syntax hints:  {crab 3443   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-ss 3993

This theorem is referenced by:  ssrab3  4105  ssrabeq  4107  iinrab2  5093  riinrab  5107  rabelpw  5354  rabexgOLD  5356  frminex  5679  wereu2  5697  predres  6371  frpomin  6372  frpoinsg  6375  wfisgOLD  6386  ssimaex  7007  f1oresrab  7161  weniso  7390  canth  7401  riotacl  7422  riotassuni  7445  onminesb  7829  onminsb  7830  onintrab  7832  onnminsb  7835  onminex  7838  tfisg  7891  tfis  7892  suppssdm  8218  fnsuppres  8232  oeeulem  8657  nnawordex  8693  pmvalg  8895  fineqvlem  9325  ordtypelem3  9589  ordtypelem4  9590  ordtypelem6  9592  hartogs  9613  card2on  9623  wdom2d  9649  oemapvali  9753  frinsg  9820  tz9.12lem1  9856  tz9.12lem3  9858  rankf  9863  cardf2  10012  cardid2  10022  cardmin2  10068  acni3  10116  dfac2a  10199  cofsmo  10338  coftr  10342  fin2i2  10387  isfin2-2  10388  enfin2i  10390  fin1a2lem11  10479  fin1a2lem12  10480  axdc3lem4  10522  ac6  10549  ondomon  10632  alephval2  10641  pwfseqlem1  10727  pwfseqlem3  10729  wunccl  10813  tskmcl  10910  infm3  12254  uzf  12906  nnwos  12980  supminf  13000  zsupss  13002  rpnnen1lem1  13043  rpnnen1lem3  13044  rpnnen1lem5  13046  ixxf  13417  fzf  13571  flval3  13866  rabssnn0fi  14037  expge0  14149  expge1  14150  hashbclem  14501  01sqrexlem3  15293  rlimrege0  15625  incexc2  15886  bitsf  16473  bitsfzolem  16480  sadadd2lem  16505  sadadd3  16507  sadcl  16508  smupf  16524  smuval2  16528  smupvallem  16529  smucl  16530  smueqlem  16536  lcmcllem  16643  lcmn0cl  16644  lcmledvds  16646  lcmfval  16668  lcmfcllem  16672  lcmfn0cl  16673  lcmfledvds  16679  phicl2  16815  phibnd  16818  hashdvds  16822  phiprmpw  16823  phimullem  16826  eulerth  16830  phisum  16837  odzcllem  16839  odzdvds  16842  prmreclem1  16963  prmreclem2  16964  prmreclem3  16965  prmreclem4  16966  prmreclem5  16967  hashbccl  17050  prmgaplem3  17100  prmgaplem4  17101  prdsds  17524  mrcflem  17664  isacs1i  17715  wunnat  18024  wunnatOLD  18025  dmcoass  18133  lublecl  18431  lubid  18432  rabsubmgmd  18742  mgmhmeql  18754  issubmd  18841  mhmeql  18861  cntzval  19361  cntzssv  19368  symgsssg  19509  symgfisg  19510  pmtrdifellem4  19521  odfval  19574  odlem1  19577  odlem2  19581  odngen  19619  gexlem1  19621  gexlem2  19624  sylow2alem2  19660  sylow2blem3  19664  oddvdssubg  19897  cyggex2  19939  ablfaclem3  20131  lssacs  20988  lspf  20995  ocvfval  21707  ocvval  21708  dsmmval2  21779  dsmmsubg  21786  asplss  21917  aspsubrg  21919  psrass1lem  21975  psrdi  22008  psrdir  22009  psrass23l  22010  psrass23  22012  resspsrmul  22019  mplbas  22033  mplsubglem  22042  mplsubrglem  22047  mplmonmul  22077  psropprmul  22260  scmatlss  22552  smadiadet  22697  pmatcoe1fsupp  22728  cpmatsubgpmat  22747  fctop  23032  cctop  23034  ppttop  23035  epttop  23037  clscld  23076  neips  23142  neiptopnei  23161  ordtbaslem  23217  ordtuni  23219  ordtcld1  23226  ordtcld2  23227  cnpfval  23263  iscnp2  23268  cmpcov2  23419  cmpsublem  23428  tgcmp  23430  conncompcld  23463  1stcfb  23474  2ndc1stc  23480  2ndcdisj  23485  finlocfin  23549  kgentopon  23567  xkotf  23614  txkgen  23681  xkococnlem  23688  imastopn  23749  kqffn  23754  opnfbas  23871  flimfnfcls  24057  alexsubALT  24080  ptcmplem2  24082  symgtgp  24135  tgpconncompeqg  24141  tgpconncomp  24142  ghmcnp  24144  tsmsfbas  24157  eltsms  24162  utoptop  24264  utopbas  24265  blfvalps  24414  blfps  24437  blf  24438  nmoffn  24753  nmofval  24756  nmogelb  24758  nmolb  24759  nmof  24761  ishtpy  25023  clsocv  25303  rrxnm  25444  rrxbasefi  25463  minveclem3b  25481  minveclem4  25485  ovolcl  25532  ovollb  25533  ovolgelb  25534  ovolge0  25535  ovolshftlem1  25563  ovolshft  25565  ovolscalem1  25567  ovolscalem2  25568  ovolsca  25569  ovolicc2lem3  25573  shftmbl  25592  iundisj  25602  dyadmax  25652  dyadmbllem  25653  opnmbllem  25655  mdegmullem  26137  uc1pval  26199  mon1pval  26201  elqaalem1  26379  elqaalem3  26381  aannenlem2  26389  aalioulem2  26393  radcnvcl  26478  radcnvlt1  26479  radcnvle  26481  ftalem4  27137  ftalem5  27138  efnnfsumcl  27164  isppw  27175  sgmval2  27204  efchtdvds  27220  sqff1o  27243  fsumdvdsdiaglem  27244  fsumdvdsdiag  27245  fsumdvdscom  27246  musum  27252  muinv  27254  sgmmul  27263  ppiub  27266  vmasum  27278  logfac2  27279  perfectlem2  27292  lgsfcl  27367  lgscl  27373  lgsquadlem1  27442  lgsquadlem2  27443  rpvmasumlem  27549  mudivsum  27592  mulogsum  27594  mulog2sumlem2  27597  vmalogdivsum2  27600  logsqvma  27604  logsqvma2  27605  selberglem3  27609  selberg  27610  selberg34r  27633  pntsval2  27638  pntrlog2bndlem1  27639  sltval2  27719  conway  27862  eqscut2  27869  scutun12  27873  scutbdaybnd  27878  scutbdaybnd2  27879  scutbdaylt  27881  bday1s  27894  cuteq0  27895  madef  27913  leftssold  27935  rightssold  27936  madebdaylemlrcut  27955  cofcut1  27972  cofcutr  27976  cutlt  27984  precsexlem8  28256  precsexlem11  28259  onssno  28295  tglnunirn  28574  tglnssp  28578  incistruhgr  29114  upgrss  29123  upgrn0  29124  upgruhgr  29137  usgrss  29209  uspgrushgr  29212  ushgredgedg  29264  ushgredgedgloop  29266  vtxdun  29517  vtxdginducedm1  29579  wlknwwlksnbij  29921  hashwwlksnext  29947  frcond3  30301  numclwlk1lem2  30402  ocsh  31315  spancl  31368  shsval2i  31419  ococin  31440  chsupid  31444  speccl  31931  hatomistici  32394  chpssati  32395  iundisjf  32611  aciunf1  32681  fpwrelmap  32747  iundisjfi  32801  pwrssmgc  32973  cycpmco2f1  33117  cycpmco2rn  33118  cycpmco2lem1  33119  cycpmco2lem2  33120  cycpmco2lem3  33121  cycpmco2lem4  33122  cycpmco2lem5  33123  cycpmco2lem6  33124  cycpmco2lem7  33125  cycpmco2  33126  nsgmgclem  33404  constrsuc  33728  locfinreflem  33786  zarclsiin  33817  zarcls  33820  zartopn  33821  esumrnmpt2  34032  esumpinfval  34037  sigagensiga  34105  ldgenpisyslem1  34127  ldgenpisys  34130  measvuni  34178  imambfm  34227  dya2iocuni  34248  omscl  34260  oms0  34262  omsmon  34263  omssubadd  34265  carsgcl  34269  oddpwdc  34319  eulerpartlem1  34332  eulerpartlemt  34336  eulerpartgbij  34337  eulerpartlemmf  34340  eulerpartlemgh  34343  eulerpartlemgs2  34345  ballotlem2  34453  ballotlemfc0  34457  ballotlemfcc  34458  ballotlemfmpn  34459  ballotlemiex  34466  ballotlemsup  34469  ballotlem7  34500  ballotth  34502  reprpmtf1o  34603  breprexplema  34607  hgt750lema  34634  bnj110  34834  bnj1204  34988  bnj1311  35000  fnrelpredd  35065  subfacp1lem6  35153  erdszelem2  35160  connpconn  35203  cvmliftmolem2  35250  cvmliftlem15  35266  cvmlift2lem12  35282  snmlff  35297  satfrnmapom  35338  rankeq1o  36135  finminlem  36284  fnessref  36323  neibastop1  36325  neibastop2lem  36326  weiunlem2  36429  weiunse  36434  bj-rabtr  36896  bj-rabtrAUTO  36898  bj-vecssmod  37247  icoreresf  37318  phpreu  37564  fin2so  37567  poimirlem26  37606  poimirlem31  37611  poimirlem32  37612  opnmbllem0  37616  mblfinlem1  37617  mblfinlem2  37618  ismblfin  37621  mbfposadd  37627  cnambfre  37628  cover2  37675  indexa  37693  fdc  37705  sstotbnd2  37734  sstotbnd3  37736  igenidl  38023  prnc  38027  toycom  38929  lkrlss  39051  atlatmstc  39275  atlatle  39276  glbconN  39333  glbconNOLD  39334  linepsubN  39709  pmapssat  39716  pmaple  39718  pmapsub  39725  paddssat  39771  diass  40999  diaglbN  41012  diaintclN  41015  diassdvaN  41017  docaclN  41081  dibglbN  41123  dibintclN  41124  diclspsn  41151  dihglblem2N  41251  dih1dimatlem  41286  dihglb2  41299  dochval2  41309  dochcl  41310  dochvalr  41314  doch2val2  41321  dochss  41322  dochocss  41323  lclkr  41490  lclkrs  41496  lcdvbase  41550  lcdvbasess  41551  mapdunirnN  41607  aks4d1p4  42036  aks4d1p5  42037  aks4d1p7  42040  aks4d1p8  42044  sticksstones1  42103  aks6d1c6lem2  42128  grpods  42151  unitscyglem1  42152  unitscyglem2  42153  unitscyglem4  42155  mhpind  42549  mhphf  42552  prjcrv0  42588  infdesc  42598  mzpindd  42702  fiphp3d  42775  rencldnfilem  42776  irrapx1  42784  pellexlem3  42787  pellfundre  42837  pellfundge  42838  pellfundlb  42840  pellfundglb  42841  jm2.22  42952  jm2.23  42953  rpnnen3  42989  pwssplit4  43046  pwfi2f1o  43053  hbtlem6  43086  dgraalem  43102  dgraaub  43105  itgocn  43121  rgspncl  43126  onintunirab  43188  nadd2rabord  43347  nadd1rabord  43351  rfovcnvf1od  43966  fsovfd  43974  fsovcnvlem  43975  binomcxplemdvbinom  44322  binomcxplemcvg  44323  binomcxplemnotnn0  44325  uzwo4  44955  disjf1o  45098  icof  45126  allbutfiinf  45335  supminfxr  45379  supminfxr2  45384  fsumsupp0  45499  sumnnodd  45551  fnlimabslt  45600  liminfvalxr  45704  ioodvbdlimc1lem1  45852  dvnprodlem1  45867  dvnprodlem2  45868  stoweidlem14  45935  stoweidlem34  45955  stoweidlem44  45965  stoweidlem50  45971  stoweidlem51  45972  stoweidlem52  45973  stoweidlem57  45978  stoweidlem59  45980  fourierdlem19  46047  fourierdlem20  46048  fourierdlem25  46053  fourierdlem31  46059  fourierdlem37  46065  fourierdlem42  46070  fourierdlem51  46078  fourierdlem54  46081  fourierdlem64  46091  fourierdlem79  46106  elaa2lem  46154  etransclem16  46171  etransclem24  46179  etransclem31  46186  etransclem33  46188  etransclem34  46189  etransclem48  46203  salgencl  46253  salexct  46255  salgenuni  46258  subsaliuncllem  46278  meadjiunlem  46386  caragenss  46425  caratheodory  46449  ovnlecvr  46479  ovnlerp  46483  ovn0lem  46486  ovnsubaddlem1  46491  hoidmv1lelem1  46512  hoidmv1lelem3  46514  hoidmvlelem1  46516  hoidmvlelem2  46517  hoidmvlelem3  46518  hoidmvlelem4  46519  ovnhoilem1  46522  ovnhoilem2  46523  ovnlecvr2  46531  ovncvr2  46532  opnvonmbllem2  46554  ovolval4lem1  46570  pimconstlt1  46623  pimiooltgt  46631  pimgtmnf2  46635  pimdecfgtioc  46636  pimincfltioc  46637  pimdecfgtioo  46638  pimincfltioo  46639  sssmf  46659  incsmflem  46662  smfaddlem1  46684  smfaddlem2  46685  decsmflem  46687  smflimlem1  46692  smflimlem2  46693  smflimlem3  46694  smfrec  46710  smfmullem4  46715  smfdiv  46718  smfsuplem1  46732  smfsuplem3  46734  smfinflem  46738  smflimsuplem1  46741  smflimsuplem7  46747  smfliminflem  46751  sprsymrelfolem1  47366  prmdvdsfmtnof1lem1  47458  prmdvdsfmtnof  47460  perfectALTVlem2  47596  isubgruhgr  47738  isubgrgrim  47781  uhgrimisgrgric  47783  uspgrlimlem1  47812  uspgrlimlem4  47815  uspgrlim  47816  grlimgrtrilem2  47819  oddibas  47896  2zlidl  47963  2zrngbas  47965  2zrng0  47967  isclatd  48655  topclat  48670