Theorem ssrab2 4043

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

Syntax hints:  {crab 3405   ⊆ wss 3914

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-ss 3931

This theorem is referenced by:  ssrab3  4045  ssrabeq  4047  iinrab2  5034  riinrab  5048  rabelpw  5291  rabexgOLD  5293  frminex  5617  wereu2  5635  predres  6312  frpomin  6313  frpoinsg  6316  ssimaex  6946  f1oresrab  7099  weniso  7329  canth  7341  riotacl  7361  riotassuni  7384  onminesb  7769  onminsb  7770  onintrab  7772  onnminsb  7775  onminex  7778  tfisg  7830  tfis  7831  suppssdm  8156  fnsuppres  8170  oeeulem  8565  nnawordex  8601  pmvalg  8810  fineqvlem  9209  ordtypelem3  9473  ordtypelem4  9474  ordtypelem6  9476  hartogs  9497  card2on  9507  wdom2d  9533  oemapvali  9637  frinsg  9704  tz9.12lem1  9740  tz9.12lem3  9742  rankf  9747  cardf2  9896  cardid2  9906  cardmin2  9952  acni3  10000  dfac2a  10083  cofsmo  10222  coftr  10226  fin2i2  10271  isfin2-2  10272  enfin2i  10274  fin1a2lem11  10363  fin1a2lem12  10364  axdc3lem4  10406  ac6  10433  ondomon  10516  alephval2  10525  pwfseqlem1  10611  pwfseqlem3  10613  wunccl  10697  tskmcl  10794  infm3  12142  uzf  12796  nnwos  12874  supminf  12894  zsupss  12896  rpnnen1lem1  12937  rpnnen1lem3  12938  rpnnen1lem5  12940  ixxf  13316  fzf  13472  flval3  13777  rabssnn0fi  13951  expge0  14063  expge1  14064  hashbclem  14417  01sqrexlem3  15210  rlimrege0  15545  incexc2  15804  bitsf  16397  bitsfzolem  16404  sadadd2lem  16429  sadadd3  16431  sadcl  16432  smupf  16448  smuval2  16452  smupvallem  16453  smucl  16454  smueqlem  16460  lcmcllem  16566  lcmn0cl  16567  lcmledvds  16569  lcmfval  16591  lcmfcllem  16595  lcmfn0cl  16596  lcmfledvds  16602  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  17567  isacs1i  17618  wunnat  17921  dmcoass  18028  lublecl  18320  lubid  18321  rabsubmgmd  18631  mgmhmeql  18643  issubmd  18733  mhmeql  18753  cntzval  19253  cntzssv  19260  symgsssg  19397  symgfisg  19398  pmtrdifellem4  19409  odfval  19462  odlem1  19465  odlem2  19469  odngen  19507  gexlem1  19509  gexlem2  19512  sylow2alem2  19548  sylow2blem3  19552  oddvdssubg  19785  cyggex2  19827  ablfaclem3  20019  rgspncl  20522  lssacs  20873  lspf  20880  ocvfval  21575  ocvval  21576  dsmmval2  21645  dsmmsubg  21652  asplss  21783  aspsubrg  21785  psrass1lem  21841  psrdi  21874  psrdir  21875  psrass23l  21876  psrass23  21878  resspsrmul  21885  mplbas  21899  mplsubglem  21908  mplsubrglem  21913  mplmonmul  21943  psropprmul  22122  scmatlss  22412  smadiadet  22557  pmatcoe1fsupp  22588  cpmatsubgpmat  22607  fctop  22891  cctop  22893  ppttop  22894  epttop  22896  clscld  22934  neips  23000  neiptopnei  23019  ordtbaslem  23075  ordtuni  23077  ordtcld1  23084  ordtcld2  23085  cnpfval  23121  iscnp2  23126  cmpcov2  23277  cmpsublem  23286  tgcmp  23288  conncompcld  23321  1stcfb  23332  2ndc1stc  23338  2ndcdisj  23343  finlocfin  23407  kgentopon  23425  xkotf  23472  txkgen  23539  xkococnlem  23546  imastopn  23607  kqffn  23612  opnfbas  23729  flimfnfcls  23915  alexsubALT  23938  ptcmplem2  23940  symgtgp  23993  tgpconncompeqg  23999  tgpconncomp  24000  ghmcnp  24002  tsmsfbas  24015  eltsms  24020  utoptop  24122  utopbas  24123  blfvalps  24271  blfps  24294  blf  24295  nmoffn  24599  nmofval  24602  nmogelb  24604  nmolb  24605  nmof  24607  ishtpy  24871  clsocv  25150  rrxnm  25291  rrxbasefi  25310  minveclem3b  25328  minveclem4  25332  ovolcl  25379  ovollb  25380  ovolgelb  25381  ovolge0  25382  ovolshftlem1  25410  ovolshft  25412  ovolscalem1  25414  ovolscalem2  25415  ovolsca  25416  ovolicc2lem3  25420  shftmbl  25439  iundisj  25449  dyadmax  25499  dyadmbllem  25500  opnmbllem  25502  mdegmullem  25983  uc1pval  26045  mon1pval  26047  elqaalem1  26227  elqaalem3  26229  aannenlem2  26237  aalioulem2  26241  radcnvcl  26326  radcnvlt1  26327  radcnvle  26329  ftalem4  26986  ftalem5  26987  efnnfsumcl  27013  isppw  27024  sgmval2  27053  efchtdvds  27069  sqff1o  27092  fsumdvdsdiaglem  27093  fsumdvdsdiag  27094  fsumdvdscom  27095  musum  27101  muinv  27103  sgmmul  27112  ppiub  27115  vmasum  27127  logfac2  27128  perfectlem2  27141  lgsfcl  27216  lgscl  27222  lgsquadlem1  27291  lgsquadlem2  27292  rpvmasumlem  27398  mudivsum  27441  mulogsum  27443  mulog2sumlem2  27446  vmalogdivsum2  27449  logsqvma  27453  logsqvma2  27454  selberglem3  27458  selberg  27459  selberg34r  27482  pntsval2  27487  pntrlog2bndlem1  27488  sltval2  27568  conway  27711  eqscut2  27718  scutun12  27722  scutbdaybnd  27727  scutbdaybnd2  27728  scutbdaylt  27730  bday1s  27743  cuteq0  27744  madef  27764  leftssold  27790  rightssold  27791  madebdaylemlrcut  27810  cofcut1  27828  cofcutr  27832  cutlt  27840  precsexlem8  28116  precsexlem11  28119  onssno  28155  onscutlt  28165  onsiso  28169  bdayon  28173  bdayn0p1  28258  tglnunirn  28475  tglnssp  28479  incistruhgr  29006  upgrss  29015  upgrn0  29016  upgruhgr  29029  usgrss  29101  uspgrushgr  29104  ushgredgedg  29156  ushgredgedgloop  29158  vtxdun  29409  vtxdginducedm1  29471  wlknwwlksnbij  29818  hashwwlksnext  29844  frcond3  30198  numclwlk1lem2  30299  ocsh  31212  spancl  31265  shsval2i  31316  ococin  31337  chsupid  31341  speccl  31828  hatomistici  32291  chpssati  32292  iundisjf  32518  aciunf1  32587  fpwrelmap  32656  iundisjfi  32719  pwrssmgc  32926  cycpmco2f1  33081  cycpmco2rn  33082  cycpmco2lem1  33083  cycpmco2lem2  33084  cycpmco2lem3  33085  cycpmco2lem4  33086  cycpmco2lem5  33087  cycpmco2lem6  33088  cycpmco2lem7  33089  cycpmco2  33090  fxpss  33123  nsgmgclem  33382  constrsuc  33728  locfinreflem  33830  zarclsiin  33861  zarcls  33864  zartopn  33865  esumrnmpt2  34058  esumpinfval  34063  sigagensiga  34131  ldgenpisyslem1  34153  ldgenpisys  34156  measvuni  34204  imambfm  34253  dya2iocuni  34274  omscl  34286  oms0  34288  omsmon  34289  omssubadd  34291  carsgcl  34295  oddpwdc  34345  eulerpartlem1  34358  eulerpartlemt  34362  eulerpartgbij  34363  eulerpartlemmf  34366  eulerpartlemgh  34369  eulerpartlemgs2  34371  ballotlem2  34480  ballotlemfc0  34484  ballotlemfcc  34485  ballotlemfmpn  34486  ballotlemiex  34493  ballotlemsup  34496  ballotlem7  34527  ballotth  34529  reprpmtf1o  34617  breprexplema  34621  hgt750lema  34648  bnj110  34848  bnj1204  35002  bnj1311  35014  fnrelpredd  35079  subfacp1lem6  35172  erdszelem2  35179  connpconn  35222  cvmliftmolem2  35269  cvmliftlem15  35285  cvmlift2lem12  35301  snmlff  35316  satfrnmapom  35357  rankeq1o  36159  finminlem  36306  fnessref  36345  neibastop1  36347  neibastop2lem  36348  weiunlem2  36451  weiunse  36456  bj-rabtr  36918  bj-rabtrAUTO  36920  bj-vecssmod  37269  icoreresf  37340  phpreu  37598  fin2so  37601  poimirlem26  37640  poimirlem31  37645  poimirlem32  37646  opnmbllem0  37650  mblfinlem1  37651  mblfinlem2  37652  ismblfin  37655  mbfposadd  37661  cnambfre  37662  cover2  37709  indexa  37727  fdc  37739  sstotbnd2  37768  sstotbnd3  37770  igenidl  38057  prnc  38061  toycom  38966  lkrlss  39088  atlatmstc  39312  atlatle  39313  glbconN  39370  glbconNOLD  39371  linepsubN  39746  pmapssat  39753  pmaple  39755  pmapsub  39762  paddssat  39808  diass  41036  diaglbN  41049  diaintclN  41052  diassdvaN  41054  docaclN  41118  dibglbN  41160  dibintclN  41161  diclspsn  41188  dihglblem2N  41288  dih1dimatlem  41323  dihglb2  41336  dochval2  41346  dochcl  41347  dochvalr  41351  doch2val2  41358  dochss  41359  dochocss  41360  lclkr  41527  lclkrs  41533  lcdvbase  41587  lcdvbasess  41588  mapdunirnN  41644  aks4d1p4  42067  aks4d1p5  42068  aks4d1p7  42071  aks4d1p8  42075  sticksstones1  42134  aks6d1c6lem2  42159  grpods  42182  unitscyglem1  42183  unitscyglem2  42184  unitscyglem4  42186  mhpind  42582  mhphf  42585  prjcrv0  42621  infdesc  42631  mzpindd  42734  fiphp3d  42807  rencldnfilem  42808  irrapx1  42816  pellexlem3  42819  pellfundre  42869  pellfundge  42870  pellfundlb  42872  pellfundglb  42873  jm2.22  42984  jm2.23  42985  rpnnen3  43021  pwssplit4  43078  pwfi2f1o  43085  hbtlem6  43118  dgraalem  43134  dgraaub  43137  itgocn  43153  onintunirab  43216  nadd2rabord  43374  nadd1rabord  43378  rfovcnvf1od  43993  fsovfd  44001  fsovcnvlem  44002  binomcxplemdvbinom  44342  binomcxplemcvg  44343  binomcxplemnotnn0  44345  uzwo4  45047  disjf1o  45185  icof  45213  allbutfiinf  45416  supminfxr  45460  supminfxr2  45465  fsumsupp0  45576  sumnnodd  45628  fnlimabslt  45677  liminfvalxr  45781  ioodvbdlimc1lem1  45929  dvnprodlem1  45944  dvnprodlem2  45945  stoweidlem14  46012  stoweidlem34  46032  stoweidlem44  46042  stoweidlem50  46048  stoweidlem51  46049  stoweidlem52  46050  stoweidlem57  46055  stoweidlem59  46057  fourierdlem19  46124  fourierdlem20  46125  fourierdlem25  46130  fourierdlem31  46136  fourierdlem37  46142  fourierdlem42  46147  fourierdlem51  46155  fourierdlem54  46158  fourierdlem64  46168  fourierdlem79  46183  elaa2lem  46231  etransclem16  46248  etransclem24  46256  etransclem31  46263  etransclem33  46265  etransclem34  46266  etransclem48  46280  salgencl  46330  salexct  46332  salgenuni  46335  subsaliuncllem  46355  meadjiunlem  46463  caragenss  46502  caratheodory  46526  ovnlecvr  46556  ovnlerp  46560  ovn0lem  46563  ovnsubaddlem1  46568  hoidmv1lelem1  46589  hoidmv1lelem3  46591  hoidmvlelem1  46593  hoidmvlelem2  46594  hoidmvlelem3  46595  hoidmvlelem4  46596  ovnhoilem1  46599  ovnhoilem2  46600  ovnlecvr2  46608  ovncvr2  46609  opnvonmbllem2  46631  ovolval4lem1  46647  pimconstlt1  46700  pimiooltgt  46708  pimgtmnf2  46712  pimdecfgtioc  46713  pimincfltioc  46714  pimdecfgtioo  46715  pimincfltioo  46716  sssmf  46736  incsmflem  46739  smfaddlem1  46761  smfaddlem2  46762  decsmflem  46764  smflimlem1  46769  smflimlem2  46770  smflimlem3  46771  smfrec  46787  smfmullem4  46792  smfdiv  46795  smfsuplem1  46809  smfsuplem3  46811  smfinflem  46815  smflimsuplem1  46818  smflimsuplem7  46824  smfliminflem  46828  sprsymrelfolem1  47493  prmdvdsfmtnof1lem1  47585  prmdvdsfmtnof  47587  perfectALTVlem2  47723  isubgredg  47866  isubgruhgr  47868  isubgrgrim  47929  uhgrimisgrgric  47931  uspgrlimlem1  47987  uspgrlimlem4  47990  uspgrlim  47991  grlimgrtrilem2  47994  oddibas  48161  2zlidl  48228  2zrngbas  48230  2zrng0  48232  isclatd  48971  topclat  48986