Theorem ssrab2 4036

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 3943	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴

Syntax hints:  {crab 3417   ⊆ wss 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-ss 3924

This theorem is referenced by:  ssrab3  4038  ssrabeq  4040  iinrab2  5029  riinrab  5045  rabelpw  5296  rabexgOLD  5298  frminex  5630  wereu2  5648  predres  6329  frpomin  6330  frpoinsg  6333  ssimaex  6956  f1oresrab  7113  weniso  7342  canth  7354  riotacl  7374  riotassuni  7397  onminesb  7780  onminsb  7781  onintrab  7783  onnminsb  7786  onminex  7789  tfisg  7838  tfis  7839  suppssdm  8161  fnsuppres  8175  oeeulem  8575  nnawordex  8611  pmvalg  8822  fineqvlem  9214  ordtypelem3  9470  ordtypelem4  9471  ordtypelem6  9473  hartogs  9494  card2on  9504  wdom2d  9530  oemapvali  9641  frinsg  9711  tz9.12lem1  9747  tz9.12lem3  9749  rankf  9754  cardf2  9917  cardid2  9927  cardmin2  9973  acni3  10019  dfac2a  10101  cofsmo  10241  coftr  10245  fin2i2  10290  isfin2-2  10291  enfin2i  10293  fin1a2lem11  10382  fin1a2lem12  10383  axdc3lem4  10425  ac6  10452  ondomon  10535  alephval2  10545  pwfseqlem1  10631  pwfseqlem3  10633  wunccl  10717  tskmcl  10814  infm3  12162  uzf  12853  nnwos  12927  supminf  12947  zsupss  12949  rpnnen1lem1  12990  rpnnen1lem3  12991  rpnnen1lem5  12993  ixxf  13370  fzf  13527  flval3  13836  rabssnn0fi  14010  expge0  14122  expge1  14123  hashbclem  14477  01sqrexlem3  15283  rlimrege0  15618  incexc2  15880  bitsf  16473  bitsfzolem  16480  sadadd2lem  16505  sadadd3  16507  sadcl  16508  smupf  16524  smuval2  16528  smupvallem  16529  smucl  16530  smueqlem  16536  lcmcllem  16642  lcmn0cl  16643  lcmledvds  16645  lcmfval  16667  lcmfcllem  16671  lcmfn0cl  16672  lcmfledvds  16678  phicl2  16815  phibnd  16818  hashdvds  16822  phiprmpw  16823  phimullem  16826  eulerth  16830  phisum  16838  odzcllem  16840  odzdvds  16843  prmreclem1  16964  prmreclem2  16965  prmreclem3  16966  prmreclem4  16967  prmreclem5  16968  hashbccl  17051  prmgaplem3  17101  prmgaplem4  17102  prdsds  17505  mrcflem  17650  isacs1i  17701  wunnat  18004  dmcoass  18111  lublecl  18403  lubid  18404  rabsubmgmd  18750  mgmhmeql  18762  issubmd  18852  mhmeql  18873  cntzval  19379  cntzssv  19386  symgsssg  19525  symgfisg  19526  pmtrdifellem4  19537  odfval  19590  odlem1  19593  odlem2  19597  odngen  19635  gexlem1  19637  gexlem2  19640  sylow2alem2  19676  sylow2blem3  19680  oddvdssubg  19913  cyggex2  19955  ablfaclem3  20147  rgspncl  20686  lssacs  21054  lspf  21061  ocvfval  21773  ocvval  21774  dsmmval2  21843  dsmmsubg  21850  asplss  21980  aspsubrg  21982  psrass1lem  22040  psrdi  22071  psrdir  22072  psrass23l  22073  psrass23  22075  resspsrmul  22082  mplbas  22096  mplsubglem  22105  mplsubrglem  22110  mplmonmul  22144  psropprmul  22354  scmatlss  22639  smadiadet  22784  pmatcoe1fsupp  22815  cpmatsubgpmat  22834  fctop  23118  cctop  23120  ppttop  23121  epttop  23123  clscld  23161  neips  23227  neiptopnei  23246  ordtbaslem  23302  ordtuni  23304  ordtcld1  23311  ordtcld2  23312  cnpfval  23348  iscnp2  23353  cmpcov2  23504  cmpsublem  23513  tgcmp  23515  conncompcld  23548  1stcfb  23559  2ndc1stc  23565  2ndcdisj  23570  finlocfin  23634  kgentopon  23652  xkotf  23699  txkgen  23766  xkococnlem  23773  imastopn  23834  kqffn  23839  opnfbas  23956  flimfnfcls  24142  alexsubALT  24165  ptcmplem2  24167  symgtgp  24220  tgpconncompeqg  24226  tgpconncomp  24227  ghmcnp  24229  tsmsfbas  24242  eltsms  24247  utoptop  24348  utopbas  24349  blfvalps  24497  blfps  24520  blf  24521  nmoffn  24825  nmofval  24828  nmogelb  24830  nmolb  24831  nmof  24833  ishtpy  25088  clsocv  25366  rrxnm  25507  rrxbasefi  25526  minveclem3b  25544  minveclem4  25548  ovolcl  25594  ovollb  25595  ovolgelb  25596  ovolge0  25597  ovolshftlem1  25625  ovolshft  25627  ovolscalem1  25629  ovolscalem2  25630  ovolsca  25631  ovolicc2lem3  25635  shftmbl  25654  iundisj  25664  dyadmax  25714  dyadmbllem  25715  opnmbllem  25717  mdegmullem  26192  uc1pval  26254  mon1pval  26256  elqaalem1  26437  elqaalem3  26439  aannenlem2  26447  aalioulem2  26451  radcnvcl  26534  radcnvlt1  26535  radcnvle  26537  ftalem4  27194  ftalem5  27195  efnnfsumcl  27221  isppw  27232  sgmval2  27261  efchtdvds  27277  sqff1o  27300  fsumdvdsdiaglem  27301  fsumdvdsdiag  27302  fsumdvdscom  27303  musum  27309  muinv  27311  sgmmul  27319  ppiub  27322  vmasum  27334  logfac2  27335  perfectlem2  27348  lgsfcl  27423  lgscl  27429  lgsquadlem1  27498  lgsquadlem2  27499  rpvmasumlem  27605  mudivsum  27648  mulogsum  27650  mulog2sumlem2  27653  vmalogdivsum2  27656  logsqvma  27660  logsqvma2  27661  selberglem3  27665  selberg  27666  selberg34r  27689  pntsval2  27694  pntrlog2bndlem1  27695  ltsval2  27774  conway  27926  eqcuts2  27933  cutsun12  27937  cutbdaybnd  27942  cutbdaybnd2  27943  cutbdaylt  27945  bday1  27961  cuteq0  27962  madef  27983  leftssold  28018  rightssold  28019  madebdaylemlrcut  28046  sltsbday  28064  cofcut1  28067  cofcutr  28071  cutlt  28079  precsexlem8  28361  precsexlem11  28364  onssno  28401  oncutlt  28411  oniso  28418  bdayons  28423  bdayn0p1  28516  tglnunirn  28771  tglnssp  28775  plngrnssp  29005  plngssp  29007  incistruhgr  29334  upgrss  29343  upgrn0  29344  upgruhgr  29357  usgrss  29429  uspgrushgr  29432  ushgredgedg  29484  ushgredgedgloop  29486  vtxdun  29736  vtxdginducedm1  29798  wlknwwlksnbij  30142  hashwwlksnext  30168  frcond3  30525  numclwlk1lem2  30626  ocsh  31540  spancl  31593  shsval2i  31644  ococin  31665  chsupid  31669  speccl  32156  hatomistici  32619  chpssati  32620  iundisjf  32840  aciunf1  32916  fpwrelmap  32986  iundisjfi  33049  pwrssmgc  33228  cycpmco2f1  33352  cycpmco2rn  33353  cycpmco2lem1  33354  cycpmco2lem2  33355  cycpmco2lem3  33356  cycpmco2lem4  33357  cycpmco2lem5  33358  cycpmco2lem6  33359  cycpmco2lem7  33360  cycpmco2  33361  fxpss  33394  nsgmgclem  33631  0mplrim  33816  selvply1rhmlemb  33821  selvply1rhm0  33828  extvfvcl  33838  mplmulmvr  33841  evlextv  33844  mplvrpmlem  33845  mplvrpmga  33847  mplvrpmrhm  33849  psrmonmul  33852  esplylem  33868  esplympl  33869  esplymhp  33870  esplyfv1  33871  esplyfv  33872  esplyfval3  33874  esplyfval1  33875  esplyfvaln  33876  constrsuc  34040  locfinreflem  34142  zarclsiin  34173  zarcls  34176  zartopn  34177  esumrnmpt2  34370  esumpinfval  34375  sigagensiga  34443  ldgenpisyslem1  34465  ldgenpisys  34468  measvuni  34516  imambfm  34564  dya2iocuni  34585  omscl  34597  oms0  34599  omsmon  34600  omssubadd  34602  carsgcl  34606  oddpwdc  34656  eulerpartlem1  34669  eulerpartlemt  34673  eulerpartgbij  34674  eulerpartlemmf  34677  eulerpartlemgh  34680  eulerpartlemgs2  34682  ballotlem2  34791  ballotlemfc0  34795  ballotlemfcc  34796  ballotlemfmpn  34797  ballotlemiex  34804  ballotlemsup  34807  ballotlem7  34838  ballotth  34840  reprpmtf1o  34925  breprexplema  34929  hgt750lema  34956  bnj110  35158  bnj1204  35312  bnj1311  35324  fnrelpredd  35392  subfacp1lem6  35543  erdszelem2  35550  connpconn  35593  cvmliftmolem2  35640  cvmliftlem15  35656  cvmlift2lem12  35672  snmlff  35687  satfrnmapom  35728  rankeq1o  36529  finminlem  36686  fnessref  36725  neibastop1  36727  neibastop2lem  36728  weiunlem  36831  weiunse  36836  bj-rabtr  37422  bj-rabtrAUTO  37424  bj-vecssmod  37780  icoreresf  37853  phpreu  38110  fin2so  38113  poimirlem26  38152  poimirlem31  38157  poimirlem32  38158  opnmbllem0  38162  mblfinlem1  38163  mblfinlem2  38164  ismblfin  38167  mbfposadd  38173  cnambfre  38174  cover2  38221  indexa  38239  fdc  38251  sstotbnd2  38280  sstotbnd3  38282  igenidl  38569  prnc  38573  toycom  39604  lkrlss  39726  atlatmstc  39950  atlatle  39951  glbconN  40008  linepsubN  40383  pmapssat  40390  pmaple  40392  pmapsub  40399  paddssat  40445  diass  41673  diaglbN  41686  diaintclN  41689  diassdvaN  41691  docaclN  41755  dibglbN  41797  dibintclN  41798  diclspsn  41825  dihglblem2N  41925  dih1dimatlem  41960  dihglb2  41973  dochval2  41983  dochcl  41984  dochvalr  41988  doch2val2  41995  dochss  41996  dochocss  41997  lclkr  42164  lclkrs  42170  lcdvbase  42224  lcdvbasess  42225  mapdunirnN  42281  aks4d1p4  42703  aks4d1p5  42704  aks4d1p7  42707  aks4d1p8  42711  sticksstones1  42770  aks6d1c6lem2  42795  grpods  42818  unitscyglem1  42819  unitscyglem2  42820  unitscyglem4  42822  mhpind  43183  mhphf  43186  prjcrv0  43222  infdesc  43232  mzpindd  43334  fiphp3d  43403  rencldnfilem  43404  irrapx1  43412  pellexlem3  43415  pellfundre  43465  pellfundge  43466  pellfundlb  43468  pellfundglb  43469  jm2.22  43579  jm2.23  43580  rpnnen3  43616  pwssplit4  43673  pwfi2f1o  43680  hbtlem6  43713  dgraalem  43729  dgraaub  43732  itgocn  43748  onintunirab  43811  nadd2rabord  43969  nadd1rabord  43973  rfovcnvf1od  44587  fsovfd  44595  fsovcnvlem  44596  binomcxplemdvbinom  44922  binomcxplemcvg  44923  binomcxplemnotnn0  44925  uzwo4  45632  disjf1o  45768  icof  45794  allbutfiinf  45993  supminfxr  46037  supminfxr2  46042  fsumsupp0  46153  sumnnodd  46205  fnlimabslt  46252  liminfvalxr  46356  ioodvbdlimc1lem1  46504  dvnprodlem1  46519  dvnprodlem2  46520  stoweidlem14  46587  stoweidlem34  46607  stoweidlem44  46617  stoweidlem50  46623  stoweidlem51  46624  stoweidlem52  46625  stoweidlem57  46630  stoweidlem59  46632  fourierdlem19  46699  fourierdlem20  46700  fourierdlem25  46705  fourierdlem31  46711  fourierdlem37  46717  fourierdlem42  46722  fourierdlem51  46730  fourierdlem54  46733  fourierdlem64  46743  fourierdlem79  46758  elaa2lem  46806  etransclem16  46823  etransclem24  46831  etransclem31  46838  etransclem33  46840  etransclem34  46841  etransclem48  46855  salgencl  46905  salexct  46907  salgenuni  46910  subsaliuncllem  46930  meadjiunlem  47038  caragenss  47077  caratheodory  47101  ovnlecvr  47131  ovnlerp  47135  ovn0lem  47138  ovnsubaddlem1  47143  hoidmv1lelem1  47164  hoidmv1lelem3  47166  hoidmvlelem1  47168  hoidmvlelem2  47169  hoidmvlelem3  47170  hoidmvlelem4  47171  ovnhoilem1  47174  ovnhoilem2  47175  ovnlecvr2  47183  ovncvr2  47184  opnvonmbllem2  47206  ovolval4lem1  47222  pimconstlt1  47275  pimgtmnf2  47287  pimdecfgtioc  47288  pimincfltioc  47289  pimdecfgtioo  47290  pimincfltioo  47291  sssmf  47311  incsmflem  47314  smfaddlem1  47336  smfaddlem2  47337  decsmflem  47339  smflimlem1  47344  smflimlem2  47345  smflimlem3  47346  smfrec  47362  smfmullem4  47367  smfdiv  47370  smfsuplem1  47384  smfsuplem3  47386  smfinflem  47390  smflimsuplem1  47393  smflimsuplem7  47399  smfliminflem  47403  sprsymrelfolem1  48097  prmdvdsfmtnof1lem1  48192  prmdvdsfmtnof  48194  perfectALTVlem2  48343  isubgredg  48487  isubgruhgr  48489  isubgrgrim  48550  uhgrimisgrgric  48552  uspgrlimlem1  48609  uspgrlimlem4  48612  uspgrlim  48613  grlimgrtrilem2  48623  oddibas  48794  2zlidl  48861  2zrngbas  48863  2zrng0  48865  isclatd  49613  topclat  49628