Theorem ssrab2 4037

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

This proof depends on syntax axioms:  {crab 3419   ⊆ wss 3908

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-ss 3925

This theorem is used by:  ssrab3  4039  ssrabeq  4041  iinrab2  5039  riinrab  5055  rabelpw  5312  frminex  5645  wereu2  5663  predres  6347  frpomin  6348  frpoinsg  6351  ssimaex  6973  f1oresrab  7130  weniso  7365  canth  7377  riotacl  7397  riotassuni  7420  onminesb  7801  onminsb  7802  onintrab  7804  onnminsb  7807  onminex  7810  tfisg  7859  tfis  7860  suppssdm  8182  fnsuppres  8196  oeeulem  8596  nnawordex  8632  pmvalg  8843  fineqvlem  9236  ordtypelem3  9492  ordtypelem4  9493  ordtypelem6  9495  hartogs  9516  card2on  9526  wdom2d  9552  oemapvali  9663  frinsg  9733  tz9.12lem1  9769  tz9.12lem3  9771  rankf  9776  cardf2  9948  cardid2  9958  cardmin2  10004  acni3  10050  dfac2a  10132  cofsmo  10271  coftr  10275  fin2i2  10320  isfin2-2  10321  enfin2i  10323  fin1a2lem11  10412  fin1a2lem12  10413  axdc3lem4  10455  ac6  10482  ondomon  10565  alephval2  10575  pwfseqlem1  10661  pwfseqlem3  10663  wunccl  10747  tskmcl  10844  infm3  12192  uzf  12883  nnwos  12957  supminf  12977  zsupss  12979  rpnnen1lem1  13020  rpnnen1lem3  13021  rpnnen1lem5  13023  ixxf  13400  fzf  13557  flval3  13868  rabssnn0fi  14042  expge0  14154  expge1  14155  hashbclem  14509  01sqrexlem3  15321  rlimrege0  15656  incexc2  15918  bitsf  16510  bitsfzolem  16517  sadadd2lem  16542  sadadd3  16544  sadcl  16545  smupf  16561  smuval2  16565  smupvallem  16566  smucl  16567  smueqlem  16573  lcmcllem  16679  lcmn0cl  16680  lcmledvds  16682  lcmfval  16704  lcmfcllem  16708  lcmfn0cl  16709  lcmfledvds  16715  phicl2  16852  phibnd  16855  hashdvds  16859  phiprmpw  16860  phimullem  16863  eulerth  16867  phisum  16875  odzcllem  16877  odzdvds  16880  prmreclem1  17001  prmreclem2  17002  prmreclem3  17003  prmreclem4  17004  prmreclem5  17005  hashbccl  17088  prmgaplem3  17138  prmgaplem4  17139  prdsds  17542  mrcflem  17687  isacs1i  17738  wunnat  18041  dmcoass  18148  lublecl  18440  lubid  18441  rabsubmgmd  18791  mgmhmeql  18803  issubmd  18895  mhmeql  18916  cntzval  19422  cntzssv  19429  symgsssg  19568  symgfisg  19569  pmtrdifellem4  19580  odfval  19633  odlem1  19636  odlem2  19640  odngen  19678  gexlem1  19680  gexlem2  19683  sylow2alem2  19719  sylow2blem3  19723  oddvdssubg  19956  cyggex2  19998  ablfaclem3  20190  rgspncl  20749  lssacs  21125  lspf  21132  ocvfval  21853  ocvval  21854  dsmmval2  21923  dsmmsubg  21930  asplss  22060  aspsubrg  22062  psrass1lem  22120  psrdi  22151  psrdir  22152  psrass23l  22153  psrass23  22155  resspsrmul  22162  mplbas  22176  mplsubglem  22185  mplsubrglem  22190  mplmonmul  22224  psropprmul  22434  scmatlss  22719  smadiadet  22864  pmatcoe1fsupp  22895  cpmatsubgpmat  22914  fctop  23198  cctop  23200  ppttop  23201  epttop  23203  clscld  23241  neips  23307  neiptopnei  23326  ordtbaslem  23382  ordtuni  23384  ordtcld1  23391  ordtcld2  23392  cnpfval  23428  iscnp2  23433  cmpcov2  23584  cmpsublem  23593  tgcmp  23595  conncompcld  23628  1stcfb  23639  2ndc1stc  23645  2ndcdisj  23650  finlocfin  23714  kgentopon  23732  xkotf  23779  txkgen  23846  xkococnlem  23853  imastopn  23914  kqffn  23919  opnfbas  24036  flimfnfcls  24222  alexsubALT  24245  ptcmplem2  24247  symgtgp  24300  tgpconncompeqg  24306  tgpconncomp  24307  ghmcnp  24309  tsmsfbas  24322  eltsms  24327  utoptop  24428  utopbas  24429  blfvalps  24577  blfps  24600  blf  24601  nmoffn  24905  nmofval  24908  nmogelb  24910  nmolb  24911  nmof  24913  ishtpy  25168  clsocv  25446  rrxnm  25587  rrxbasefi  25606  minveclem3b  25624  minveclem4  25628  ovolcl  25674  ovollb  25675  ovolgelb  25676  ovolge0  25677  ovolshftlem1  25705  ovolshft  25707  ovolscalem1  25709  ovolscalem2  25710  ovolsca  25711  ovolicc2lem3  25715  shftmbl  25734  iundisj  25744  dyadmax  25794  dyadmbllem  25795  opnmbllem  25797  mdegmullem  26272  uc1pval  26334  mon1pval  26336  elqaalem1  26517  elqaalem3  26519  aannenlem2  26529  aalioulem2  26533  radcnvcl  26617  radcnvlt1  26618  radcnvle  26620  ftalem4  27277  ftalem5  27278  efnnfsumcl  27304  isppw  27315  sgmval2  27344  efchtdvds  27360  sqff1o  27383  fsumdvdsdiaglem  27384  fsumdvdsdiag  27385  fsumdvdscom  27386  musum  27392  muinv  27394  sgmmul  27402  ppiub  27405  vmasum  27417  logfac2  27418  perfectlem2  27431  lgsfcl  27506  lgscl  27512  lgsquadlem1  27581  lgsquadlem2  27582  rpvmasumlem  27688  mudivsum  27731  mulogsum  27733  mulog2sumlem2  27736  vmalogdivsum2  27739  logsqvma  27743  logsqvma2  27744  selberglem3  27748  selberg  27749  selberg34r  27772  pntsval2  27777  pntrlog2bndlem1  27778  ltsval2  27857  conway  28009  eqcuts2  28016  cutsun12  28020  cutbdaybnd  28025  cutbdaybnd2  28026  cutbdaylt  28028  bday1  28044  cuteq0  28045  madef  28066  leftssold  28101  rightssold  28102  madebdaylemlrcut  28129  sltsbday  28147  cofcut1  28150  cofcutr  28154  cutlt  28162  precsexlem8  28444  precsexlem11  28447  onssno  28484  oncutlt  28494  oniso  28501  bdayons  28506  bdayn0p1  28599  tglnunirn  28854  tglnssp  28858  plngrnssp  29098  plngssp  29100  incistruhgr  29466  upgrss  29475  upgrn0  29476  upgruhgr  29489  usgrss  29561  uspgrushgr  29564  ushgredgedg  29616  ushgredgedgloop  29618  vtxdun  29868  vtxdginducedm1  29930  wlknwwlksnbij  30274  hashwwlksnext  30300  frcond3  30657  numclwlk1lem2  30758  ocsh  31672  spancl  31725  shsval2i  31776  ococin  31797  chsupid  31801  speccl  32288  hatomistici  32751  chpssati  32752  iundisjf  32971  aciunf1  33045  fpwrelmap  33115  iundisjfi  33178  pwrssmgc  33351  cycpmco2f1  33475  cycpmco2rn  33476  cycpmco2lem1  33477  cycpmco2lem2  33478  cycpmco2lem3  33479  cycpmco2lem4  33480  cycpmco2lem5  33481  cycpmco2lem6  33482  cycpmco2lem7  33483  cycpmco2  33484  fxpss  33517  nsgmgclem  33751  0mplrim  33935  selvply1rhmlemb  33940  selvply1rhm0  33947  extvfvcl  33957  mplmulmvr  33960  evlextv  33963  mplvrpmlem  33964  mplvrpmga  33966  mplvrpmrhm  33968  psrmonmul  33971  esplylem  33987  esplympl  33988  esplymhp  33989  esplyfv1  33990  esplyfv  33991  esplyfval3  33993  esplyfval1  33994  esplyfvaln  33995  constrsuc  34159  locfinreflem  34261  zarclsiin  34292  zarcls  34295  zartopn  34296  esumrnmpt2  34489  esumpinfval  34494  sigagensiga  34563  ldgenpisyslem1  34585  ldgenpisys  34588  measvuni  34636  imambfm  34684  dya2iocuni  34705  omscl  34717  oms0  34719  omsmon  34720  omssubadd  34722  carsgcl  34726  oddpwdc  34776  eulerpartlem1  34789  eulerpartlemt  34793  eulerpartgbij  34794  eulerpartlemmf  34797  eulerpartlemgh  34800  eulerpartlemgs2  34802  ballotlem2  34911  ballotlemfc0  34915  ballotlemfcc  34916  ballotlemfmpn  34917  ballotlemiex  34924  ballotlemsup  34927  ballotlem7  34958  ballotth  34960  reprpmtf1o  35045  breprexplema  35049  hgt750lema  35076  bnj110  35278  bnj1204  35432  bnj1311  35444  fnrelpredd  35507  subfacp1lem6  35698  erdszelem2  35705  connpconn  35748  cvmliftmolem2  35795  cvmliftlem15  35811  cvmlift2lem12  35827  snmlff  35842  satfrnmapom  35883  rankeq1o  36684  nmuladdel  36725  finminlem  36870  fnessref  36909  neibastop1  36911  neibastop2lem  36912  weiunlem  37015  weiunse  37020  bj-rabtr  37607  bj-rabtrAUTO  37609  bj-vecssmod  37966  icoreresf  38039  phpreu  38296  fin2so  38299  poimirlem26  38338  poimirlem31  38343  poimirlem32  38344  opnmbllem0  38348  mblfinlem1  38349  mblfinlem2  38350  ismblfin  38353  mbfposadd  38359  cnambfre  38360  cover2  38407  indexa  38425  fdc  38437  sstotbnd2  38466  sstotbnd3  38468  igenidl  38755  prnc  38759  toycom  39788  lkrlss  39910  atlatmstc  40134  atlatle  40135  glbconN  40192  linepsubN  40567  pmapssat  40574  pmaple  40576  pmapsub  40583  paddssat  40629  diass  41857  diaglbN  41870  diaintclN  41873  diassdvaN  41875  docaclN  41939  dibglbN  41981  dibintclN  41982  diclspsn  42009  dihglblem2N  42109  dih1dimatlem  42144  dihglb2  42157  dochval2  42167  dochcl  42168  dochvalr  42172  doch2val2  42179  dochss  42180  dochocss  42181  lclkr  42348  lclkrs  42354  lcdvbase  42408  lcdvbasess  42409  mapdunirnN  42465  aks4d1p4  42887  aks4d1p5  42888  aks4d1p7  42891  aks4d1p8  42895  sticksstones1  42954  aks6d1c6lem2  42979  grpods  43002  unitscyglem1  43003  unitscyglem2  43004  unitscyglem4  43006  mhpind  43367  mhphf  43370  prjcrv0  43406  infdesc  43416  mzpindd  43518  fiphp3d  43587  rencldnfilem  43588  irrapx1  43596  pellexlem3  43599  pellfundre  43649  pellfundge  43650  pellfundlb  43652  pellfundglb  43653  jm2.22  43763  jm2.23  43764  rpnnen3  43800  pwssplit4  43857  pwfi2f1o  43864  hbtlem6  43897  dgraalem  43913  dgraaub  43916  itgocn  43932  onintunirab  43995  nadd2rabord  44153  nadd1rabord  44157  rfovcnvf1od  44771  fsovfd  44779  fsovcnvlem  44780  binomcxplemdvbinom  45104  binomcxplemcvg  45105  binomcxplemnotnn0  45107  uzwo4  45814  disjf1o  45950  icof  45976  allbutfiinf  46175  supminfxr  46219  supminfxr2  46224  fsumsupp0  46335  sumnnodd  46387  fnlimabslt  46434  liminfvalxr  46538  ioodvbdlimc1lem1  46686  dvnprodlem1  46701  dvnprodlem2  46702  stoweidlem14  46769  stoweidlem34  46789  stoweidlem44  46799  stoweidlem50  46805  stoweidlem51  46806  stoweidlem52  46807  stoweidlem57  46812  stoweidlem59  46814  fourierdlem19  46881  fourierdlem20  46882  fourierdlem25  46887  fourierdlem31  46893  fourierdlem37  46899  fourierdlem42  46904  fourierdlem51  46912  fourierdlem54  46915  fourierdlem64  46925  fourierdlem79  46940  elaa2lem  46988  etransclem16  47005  etransclem24  47013  etransclem31  47020  etransclem33  47022  etransclem34  47023  etransclem48  47037  salgencl  47087  salexct  47089  salgenuni  47092  subsaliuncllem  47112  meadjiunlem  47220  caragenss  47259  caratheodory  47283  ovnlecvr  47313  ovnlerp  47317  ovn0lem  47320  ovnsubaddlem1  47325  hoidmv1lelem1  47346  hoidmv1lelem3  47348  hoidmvlelem1  47350  hoidmvlelem2  47351  hoidmvlelem3  47352  hoidmvlelem4  47353  ovnhoilem1  47356  ovnhoilem2  47357  ovnlecvr2  47365  ovncvr2  47366  opnvonmbllem2  47388  ovolval4lem1  47404  pimconstlt1  47457  pimgtmnf2  47469  pimdecfgtioc  47470  pimincfltioc  47471  pimdecfgtioo  47472  pimincfltioo  47473  sssmf  47493  incsmflem  47496  smfaddlem1  47518  smfaddlem2  47519  decsmflem  47521  smflimlem1  47526  smflimlem2  47527  smflimlem3  47528  smfrec  47544  smfmullem4  47549  smfdiv  47552  smfpimcclem  47562  smfsuplem1  47566  smfsuplem3  47568  smfinflem  47572  smflimsuplem1  47575  smflimsuplem7  47581  smfliminflem  47585  sprsymrelfolem1  48282  prmdvdsfmtnof1lem1  48377  prmdvdsfmtnof  48379  perfectALTVlem2  48528  isubgredg  48672  isubgruhgr  48674  isubgrgrim  48735  uhgrimisgrgric  48737  uspgrlimlem1  48794  uspgrlimlem4  48797  uspgrlim  48798  grlimgrtrilem2  48808  oddibas  48979  2zlidl  49046  2zrngbas  49048  2zrng0  49050  isclatd  49802  topclat  49817