Theorem ssrab2 4055

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

Syntax hints:  {crab 3415   ⊆ wss 3926

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-ss 3943

This theorem is referenced by:  ssrab3  4057  ssrabeq  4059  iinrab2  5046  riinrab  5060  rabelpw  5306  rabexgOLD  5308  frminex  5633  wereu2  5651  predres  6328  frpomin  6329  frpoinsg  6332  wfisgOLD  6343  ssimaex  6963  f1oresrab  7116  weniso  7346  canth  7357  riotacl  7377  riotassuni  7400  onminesb  7785  onminsb  7786  onintrab  7788  onnminsb  7791  onminex  7794  tfisg  7847  tfis  7848  suppssdm  8174  fnsuppres  8188  oeeulem  8611  nnawordex  8647  pmvalg  8849  fineqvlem  9268  ordtypelem3  9532  ordtypelem4  9533  ordtypelem6  9535  hartogs  9556  card2on  9566  wdom2d  9592  oemapvali  9696  frinsg  9763  tz9.12lem1  9799  tz9.12lem3  9801  rankf  9806  cardf2  9955  cardid2  9965  cardmin2  10011  acni3  10059  dfac2a  10142  cofsmo  10281  coftr  10285  fin2i2  10330  isfin2-2  10331  enfin2i  10333  fin1a2lem11  10422  fin1a2lem12  10423  axdc3lem4  10465  ac6  10492  ondomon  10575  alephval2  10584  pwfseqlem1  10670  pwfseqlem3  10672  wunccl  10756  tskmcl  10853  infm3  12199  uzf  12853  nnwos  12929  supminf  12949  zsupss  12951  rpnnen1lem1  12992  rpnnen1lem3  12993  rpnnen1lem5  12995  ixxf  13370  fzf  13526  flval3  13830  rabssnn0fi  14002  expge0  14114  expge1  14115  hashbclem  14468  01sqrexlem3  15261  rlimrege0  15593  incexc2  15852  bitsf  16444  bitsfzolem  16451  sadadd2lem  16476  sadadd3  16478  sadcl  16479  smupf  16495  smuval2  16499  smupvallem  16500  smucl  16501  smueqlem  16507  lcmcllem  16613  lcmn0cl  16614  lcmledvds  16616  lcmfval  16638  lcmfcllem  16642  lcmfn0cl  16643  lcmfledvds  16649  phicl2  16785  phibnd  16788  hashdvds  16792  phiprmpw  16793  phimullem  16796  eulerth  16800  phisum  16808  odzcllem  16810  odzdvds  16813  prmreclem1  16934  prmreclem2  16935  prmreclem3  16936  prmreclem4  16937  prmreclem5  16938  hashbccl  17021  prmgaplem3  17071  prmgaplem4  17072  prdsds  17476  mrcflem  17616  isacs1i  17667  wunnat  17970  dmcoass  18077  lublecl  18369  lubid  18370  rabsubmgmd  18680  mgmhmeql  18692  issubmd  18782  mhmeql  18802  cntzval  19302  cntzssv  19309  symgsssg  19446  symgfisg  19447  pmtrdifellem4  19458  odfval  19511  odlem1  19514  odlem2  19518  odngen  19556  gexlem1  19558  gexlem2  19561  sylow2alem2  19597  sylow2blem3  19601  oddvdssubg  19834  cyggex2  19876  ablfaclem3  20068  rgspncl  20571  lssacs  20922  lspf  20929  ocvfval  21624  ocvval  21625  dsmmval2  21694  dsmmsubg  21701  asplss  21832  aspsubrg  21834  psrass1lem  21890  psrdi  21923  psrdir  21924  psrass23l  21925  psrass23  21927  resspsrmul  21934  mplbas  21948  mplsubglem  21957  mplsubrglem  21962  mplmonmul  21992  psropprmul  22171  scmatlss  22461  smadiadet  22606  pmatcoe1fsupp  22637  cpmatsubgpmat  22656  fctop  22940  cctop  22942  ppttop  22943  epttop  22945  clscld  22983  neips  23049  neiptopnei  23068  ordtbaslem  23124  ordtuni  23126  ordtcld1  23133  ordtcld2  23134  cnpfval  23170  iscnp2  23175  cmpcov2  23326  cmpsublem  23335  tgcmp  23337  conncompcld  23370  1stcfb  23381  2ndc1stc  23387  2ndcdisj  23392  finlocfin  23456  kgentopon  23474  xkotf  23521  txkgen  23588  xkococnlem  23595  imastopn  23656  kqffn  23661  opnfbas  23778  flimfnfcls  23964  alexsubALT  23987  ptcmplem2  23989  symgtgp  24042  tgpconncompeqg  24048  tgpconncomp  24049  ghmcnp  24051  tsmsfbas  24064  eltsms  24069  utoptop  24171  utopbas  24172  blfvalps  24320  blfps  24343  blf  24344  nmoffn  24648  nmofval  24651  nmogelb  24653  nmolb  24654  nmof  24656  ishtpy  24920  clsocv  25200  rrxnm  25341  rrxbasefi  25360  minveclem3b  25378  minveclem4  25382  ovolcl  25429  ovollb  25430  ovolgelb  25431  ovolge0  25432  ovolshftlem1  25460  ovolshft  25462  ovolscalem1  25464  ovolscalem2  25465  ovolsca  25466  ovolicc2lem3  25470  shftmbl  25489  iundisj  25499  dyadmax  25549  dyadmbllem  25550  opnmbllem  25552  mdegmullem  26033  uc1pval  26095  mon1pval  26097  elqaalem1  26277  elqaalem3  26279  aannenlem2  26287  aalioulem2  26291  radcnvcl  26376  radcnvlt1  26377  radcnvle  26379  ftalem4  27036  ftalem5  27037  efnnfsumcl  27063  isppw  27074  sgmval2  27103  efchtdvds  27119  sqff1o  27142  fsumdvdsdiaglem  27143  fsumdvdsdiag  27144  fsumdvdscom  27145  musum  27151  muinv  27153  sgmmul  27162  ppiub  27165  vmasum  27177  logfac2  27178  perfectlem2  27191  lgsfcl  27266  lgscl  27272  lgsquadlem1  27341  lgsquadlem2  27342  rpvmasumlem  27448  mudivsum  27491  mulogsum  27493  mulog2sumlem2  27496  vmalogdivsum2  27499  logsqvma  27503  logsqvma2  27504  selberglem3  27508  selberg  27509  selberg34r  27532  pntsval2  27537  pntrlog2bndlem1  27538  sltval2  27618  conway  27761  eqscut2  27768  scutun12  27772  scutbdaybnd  27777  scutbdaybnd2  27778  scutbdaylt  27780  bday1s  27793  cuteq0  27794  madef  27812  leftssold  27834  rightssold  27835  madebdaylemlrcut  27854  cofcut1  27871  cofcutr  27875  cutlt  27883  precsexlem8  28155  precsexlem11  28158  onssno  28194  tglnunirn  28473  tglnssp  28477  incistruhgr  29004  upgrss  29013  upgrn0  29014  upgruhgr  29027  usgrss  29099  uspgrushgr  29102  ushgredgedg  29154  ushgredgedgloop  29156  vtxdun  29407  vtxdginducedm1  29469  wlknwwlksnbij  29816  hashwwlksnext  29842  frcond3  30196  numclwlk1lem2  30297  ocsh  31210  spancl  31263  shsval2i  31314  ococin  31335  chsupid  31339  speccl  31826  hatomistici  32289  chpssati  32290  iundisjf  32516  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  nsgmgclem  33372  constrsuc  33718  locfinreflem  33817  zarclsiin  33848  zarcls  33851  zartopn  33852  esumrnmpt2  34045  esumpinfval  34050  sigagensiga  34118  ldgenpisyslem1  34140  ldgenpisys  34143  measvuni  34191  imambfm  34240  dya2iocuni  34261  omscl  34273  oms0  34275  omsmon  34276  omssubadd  34278  carsgcl  34282  oddpwdc  34332  eulerpartlem1  34345  eulerpartlemt  34349  eulerpartgbij  34350  eulerpartlemmf  34353  eulerpartlemgh  34356  eulerpartlemgs2  34358  ballotlem2  34467  ballotlemfc0  34471  ballotlemfcc  34472  ballotlemfmpn  34473  ballotlemiex  34480  ballotlemsup  34483  ballotlem7  34514  ballotth  34516  reprpmtf1o  34604  breprexplema  34608  hgt750lema  34635  bnj110  34835  bnj1204  34989  bnj1311  35001  fnrelpredd  35066  subfacp1lem6  35153  erdszelem2  35160  connpconn  35203  cvmliftmolem2  35250  cvmliftlem15  35266  cvmlift2lem12  35282  snmlff  35297  satfrnmapom  35338  rankeq1o  36135  finminlem  36282  fnessref  36321  neibastop1  36323  neibastop2lem  36324  weiunlem2  36427  weiunse  36432  bj-rabtr  36894  bj-rabtrAUTO  36896  bj-vecssmod  37245  icoreresf  37316  phpreu  37574  fin2so  37577  poimirlem26  37616  poimirlem31  37621  poimirlem32  37622  opnmbllem0  37626  mblfinlem1  37627  mblfinlem2  37628  ismblfin  37631  mbfposadd  37637  cnambfre  37638  cover2  37685  indexa  37703  fdc  37715  sstotbnd2  37744  sstotbnd3  37746  igenidl  38033  prnc  38037  toycom  38937  lkrlss  39059  atlatmstc  39283  atlatle  39284  glbconN  39341  glbconNOLD  39342  linepsubN  39717  pmapssat  39724  pmaple  39726  pmapsub  39733  paddssat  39779  diass  41007  diaglbN  41020  diaintclN  41023  diassdvaN  41025  docaclN  41089  dibglbN  41131  dibintclN  41132  diclspsn  41159  dihglblem2N  41259  dih1dimatlem  41294  dihglb2  41307  dochval2  41317  dochcl  41318  dochvalr  41322  doch2val2  41329  dochss  41330  dochocss  41331  lclkr  41498  lclkrs  41504  lcdvbase  41558  lcdvbasess  41559  mapdunirnN  41615  aks4d1p4  42038  aks4d1p5  42039  aks4d1p7  42042  aks4d1p8  42046  sticksstones1  42105  aks6d1c6lem2  42130  grpods  42153  unitscyglem1  42154  unitscyglem2  42155  unitscyglem4  42157  mhpind  42564  mhphf  42567  prjcrv0  42603  infdesc  42613  mzpindd  42716  fiphp3d  42789  rencldnfilem  42790  irrapx1  42798  pellexlem3  42801  pellfundre  42851  pellfundge  42852  pellfundlb  42854  pellfundglb  42855  jm2.22  42966  jm2.23  42967  rpnnen3  43003  pwssplit4  43060  pwfi2f1o  43067  hbtlem6  43100  dgraalem  43116  dgraaub  43119  itgocn  43135  onintunirab  43198  nadd2rabord  43356  nadd1rabord  43360  rfovcnvf1od  43975  fsovfd  43983  fsovcnvlem  43984  binomcxplemdvbinom  44325  binomcxplemcvg  44326  binomcxplemnotnn0  44328  uzwo4  45025  disjf1o  45163  icof  45191  allbutfiinf  45395  supminfxr  45439  supminfxr2  45444  fsumsupp0  45555  sumnnodd  45607  fnlimabslt  45656  liminfvalxr  45760  ioodvbdlimc1lem1  45908  dvnprodlem1  45923  dvnprodlem2  45924  stoweidlem14  45991  stoweidlem34  46011  stoweidlem44  46021  stoweidlem50  46027  stoweidlem51  46028  stoweidlem52  46029  stoweidlem57  46034  stoweidlem59  46036  fourierdlem19  46103  fourierdlem20  46104  fourierdlem25  46109  fourierdlem31  46115  fourierdlem37  46121  fourierdlem42  46126  fourierdlem51  46134  fourierdlem54  46137  fourierdlem64  46147  fourierdlem79  46162  elaa2lem  46210  etransclem16  46227  etransclem24  46235  etransclem31  46242  etransclem33  46244  etransclem34  46245  etransclem48  46259  salgencl  46309  salexct  46311  salgenuni  46314  subsaliuncllem  46334  meadjiunlem  46442  caragenss  46481  caratheodory  46505  ovnlecvr  46535  ovnlerp  46539  ovn0lem  46542  ovnsubaddlem1  46547  hoidmv1lelem1  46568  hoidmv1lelem3  46570  hoidmvlelem1  46572  hoidmvlelem2  46573  hoidmvlelem3  46574  hoidmvlelem4  46575  ovnhoilem1  46578  ovnhoilem2  46579  ovnlecvr2  46587  ovncvr2  46588  opnvonmbllem2  46610  ovolval4lem1  46626  pimconstlt1  46679  pimiooltgt  46687  pimgtmnf2  46691  pimdecfgtioc  46692  pimincfltioc  46693  pimdecfgtioo  46694  pimincfltioo  46695  sssmf  46715  incsmflem  46718  smfaddlem1  46740  smfaddlem2  46741  decsmflem  46743  smflimlem1  46748  smflimlem2  46749  smflimlem3  46750  smfrec  46766  smfmullem4  46771  smfdiv  46774  smfsuplem1  46788  smfsuplem3  46790  smfinflem  46794  smflimsuplem1  46797  smflimsuplem7  46803  smfliminflem  46807  sprsymrelfolem1  47454  prmdvdsfmtnof1lem1  47546  prmdvdsfmtnof  47548  perfectALTVlem2  47684  isubgredg  47827  isubgruhgr  47829  isubgrgrim  47890  uhgrimisgrgric  47892  uspgrlimlem1  47948  uspgrlimlem4  47951  uspgrlim  47952  grlimgrtrilem2  47955  oddibas  48096  2zlidl  48163  2zrngbas  48165  2zrng0  48167  isclatd  48905  topclat  48920