Theorem ssrab2 4033

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

Syntax hints:  {crab 3413   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-ss 3921

This theorem is referenced by:  ssrab3  4035  ssrabeq  4037  iinrab2  5026  riinrab  5040  rabelpw  5291  rabexgOLD  5293  frminex  5624  wereu2  5642  predres  6322  frpomin  6323  frpoinsg  6326  ssimaex  6948  f1oresrab  7105  weniso  7334  canth  7346  riotacl  7366  riotassuni  7389  onminesb  7772  onminsb  7773  onintrab  7775  onnminsb  7778  onminex  7781  tfisg  7830  tfis  7831  suppssdm  8152  fnsuppres  8166  oeeulem  8566  nnawordex  8602  pmvalg  8814  fineqvlem  9206  ordtypelem3  9465  ordtypelem4  9466  ordtypelem6  9468  hartogs  9489  card2on  9499  wdom2d  9525  oemapvali  9636  frinsg  9706  tz9.12lem1  9742  tz9.12lem3  9744  rankf  9749  cardf2  9898  cardid2  9908  cardmin2  9954  acni3  10000  dfac2a  10083  cofsmo  10223  coftr  10227  fin2i2  10272  isfin2-2  10273  enfin2i  10275  fin1a2lem11  10364  fin1a2lem12  10365  axdc3lem4  10407  ac6  10434  ondomon  10517  alephval2  10527  pwfseqlem1  10613  pwfseqlem3  10615  wunccl  10699  tskmcl  10796  infm3  12148  uzf  12839  nnwos  12913  supminf  12933  zsupss  12935  rpnnen1lem1  12976  rpnnen1lem3  12977  rpnnen1lem5  12979  ixxf  13356  fzf  13513  flval3  13822  rabssnn0fi  13996  expge0  14108  expge1  14109  hashbclem  14462  01sqrexlem3  15254  rlimrege0  15589  incexc2  15851  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  16786  phibnd  16789  hashdvds  16793  phiprmpw  16794  phimullem  16797  eulerth  16801  phisum  16809  odzcllem  16811  odzdvds  16814  prmreclem1  16935  prmreclem2  16936  prmreclem3  16937  prmreclem4  16938  prmreclem5  16939  hashbccl  17022  prmgaplem3  17072  prmgaplem4  17073  prdsds  17476  mrcflem  17621  isacs1i  17672  wunnat  17975  dmcoass  18082  lublecl  18374  lubid  18375  rabsubmgmd  18721  mgmhmeql  18733  issubmd  18823  mhmeql  18843  cntzval  19344  cntzssv  19351  symgsssg  19490  symgfisg  19491  pmtrdifellem4  19502  odfval  19555  odlem1  19558  odlem2  19562  odngen  19600  gexlem1  19602  gexlem2  19605  sylow2alem2  19641  sylow2blem3  19645  oddvdssubg  19878  cyggex2  19920  ablfaclem3  20112  rgspncl  20642  lssacs  21014  lspf  21021  ocvfval  21698  ocvval  21699  dsmmval2  21768  dsmmsubg  21775  asplss  21905  aspsubrg  21907  psrass1lem  21965  psrdi  21996  psrdir  21997  psrass23l  21998  psrass23  22000  resspsrmul  22007  mplbas  22021  mplsubglem  22030  mplsubrglem  22035  mplmonmul  22069  psropprmul  22279  scmatlss  22565  smadiadet  22710  pmatcoe1fsupp  22741  cpmatsubgpmat  22760  fctop  23044  cctop  23046  ppttop  23047  epttop  23049  clscld  23087  neips  23153  neiptopnei  23172  ordtbaslem  23228  ordtuni  23230  ordtcld1  23237  ordtcld2  23238  cnpfval  23274  iscnp2  23279  cmpcov2  23430  cmpsublem  23439  tgcmp  23441  conncompcld  23474  1stcfb  23485  2ndc1stc  23491  2ndcdisj  23496  finlocfin  23560  kgentopon  23578  xkotf  23625  txkgen  23692  xkococnlem  23699  imastopn  23760  kqffn  23765  opnfbas  23882  flimfnfcls  24068  alexsubALT  24091  ptcmplem2  24093  symgtgp  24146  tgpconncompeqg  24152  tgpconncomp  24153  ghmcnp  24155  tsmsfbas  24168  eltsms  24173  utoptop  24274  utopbas  24275  blfvalps  24423  blfps  24446  blf  24447  nmoffn  24751  nmofval  24754  nmogelb  24756  nmolb  24757  nmof  24759  ishtpy  25014  clsocv  25292  rrxnm  25433  rrxbasefi  25452  minveclem3b  25470  minveclem4  25474  ovolcl  25520  ovollb  25521  ovolgelb  25522  ovolge0  25523  ovolshftlem1  25551  ovolshft  25553  ovolscalem1  25555  ovolscalem2  25556  ovolsca  25557  ovolicc2lem3  25561  shftmbl  25580  iundisj  25590  dyadmax  25640  dyadmbllem  25641  opnmbllem  25643  mdegmullem  26118  uc1pval  26180  mon1pval  26182  elqaalem1  26360  elqaalem3  26362  aannenlem2  26370  aalioulem2  26374  radcnvcl  26457  radcnvlt1  26458  radcnvle  26460  ftalem4  27117  ftalem5  27118  efnnfsumcl  27144  isppw  27155  sgmval2  27184  efchtdvds  27200  sqff1o  27223  fsumdvdsdiaglem  27224  fsumdvdsdiag  27225  fsumdvdscom  27226  musum  27232  muinv  27234  sgmmul  27242  ppiub  27245  vmasum  27257  logfac2  27258  perfectlem2  27271  lgsfcl  27346  lgscl  27352  lgsquadlem1  27421  lgsquadlem2  27422  rpvmasumlem  27528  mudivsum  27571  mulogsum  27573  mulog2sumlem2  27576  vmalogdivsum2  27579  logsqvma  27583  logsqvma2  27584  selberglem3  27588  selberg  27589  selberg34r  27612  pntsval2  27617  pntrlog2bndlem1  27618  ltsval2  27697  conway  27849  eqcuts2  27856  cutsun12  27860  cutbdaybnd  27865  cutbdaybnd2  27866  cutbdaylt  27868  bday1  27884  cuteq0  27885  madef  27906  leftssold  27941  rightssold  27942  madebdaylemlrcut  27969  sltsbday  27987  cofcut1  27990  cofcutr  27994  cutlt  28002  precsexlem8  28284  precsexlem11  28287  onssno  28324  oncutlt  28334  oniso  28341  bdayons  28346  bdayn0p1  28439  tglnunirn  28694  tglnssp  28698  incistruhgr  29226  upgrss  29235  upgrn0  29236  upgruhgr  29249  usgrss  29321  uspgrushgr  29324  ushgredgedg  29376  ushgredgedgloop  29378  vtxdun  29628  vtxdginducedm1  29690  wlknwwlksnbij  30034  hashwwlksnext  30060  frcond3  30417  numclwlk1lem2  30518  ocsh  31432  spancl  31485  shsval2i  31536  ococin  31557  chsupid  31561  speccl  32048  hatomistici  32511  chpssati  32512  iundisjf  32738  aciunf1  32815  fpwrelmap  32885  iundisjfi  32948  pwrssmgc  33139  cycpmco2f1  33265  cycpmco2rn  33266  cycpmco2lem1  33267  cycpmco2lem2  33268  cycpmco2lem3  33269  cycpmco2lem4  33270  cycpmco2lem5  33271  cycpmco2lem6  33272  cycpmco2lem7  33273  cycpmco2  33274  fxpss  33307  nsgmgclem  33558  0mplrim  33772  selvply1rhmlemb  33777  selvply1rhm0  33784  extvfvcl  33794  mplmulmvr  33797  evlextv  33800  mplvrpmlem  33801  mplvrpmga  33803  mplvrpmrhm  33805  psrmonmul  33808  esplylem  33824  esplympl  33825  esplymhp  33826  esplyfv1  33827  esplyfv  33828  esplyfval3  33830  esplyfval1  33831  esplyfvaln  33832  constrsuc  33996  locfinreflem  34098  zarclsiin  34129  zarcls  34132  zartopn  34133  esumrnmpt2  34326  esumpinfval  34331  sigagensiga  34399  ldgenpisyslem1  34421  ldgenpisys  34424  measvuni  34472  imambfm  34520  dya2iocuni  34541  omscl  34553  oms0  34555  omsmon  34556  omssubadd  34558  carsgcl  34562  oddpwdc  34612  eulerpartlem1  34625  eulerpartlemt  34629  eulerpartgbij  34630  eulerpartlemmf  34633  eulerpartlemgh  34636  eulerpartlemgs2  34638  ballotlem2  34747  ballotlemfc0  34751  ballotlemfcc  34752  ballotlemfmpn  34753  ballotlemiex  34760  ballotlemsup  34763  ballotlem7  34794  ballotth  34796  reprpmtf1o  34884  breprexplema  34888  hgt750lema  34915  bnj110  35117  bnj1204  35271  bnj1311  35283  fnrelpredd  35351  subfacp1lem6  35499  erdszelem2  35506  connpconn  35549  cvmliftmolem2  35596  cvmliftlem15  35612  cvmlift2lem12  35628  snmlff  35643  satfrnmapom  35684  rankeq1o  36485  finminlem  36642  fnessref  36681  neibastop1  36683  neibastop2lem  36684  weiunlem  36787  weiunse  36792  bj-rabtr  37379  bj-rabtrAUTO  37381  bj-vecssmod  37737  icoreresf  37810  phpreu  38067  fin2so  38070  poimirlem26  38109  poimirlem31  38114  poimirlem32  38115  opnmbllem0  38119  mblfinlem1  38120  mblfinlem2  38121  ismblfin  38124  mbfposadd  38130  cnambfre  38131  cover2  38178  indexa  38196  fdc  38208  sstotbnd2  38237  sstotbnd3  38239  igenidl  38526  prnc  38530  toycom  39561  lkrlss  39683  atlatmstc  39907  atlatle  39908  glbconN  39965  linepsubN  40340  pmapssat  40347  pmaple  40349  pmapsub  40356  paddssat  40402  diass  41630  diaglbN  41643  diaintclN  41646  diassdvaN  41648  docaclN  41712  dibglbN  41754  dibintclN  41755  diclspsn  41782  dihglblem2N  41882  dih1dimatlem  41917  dihglb2  41930  dochval2  41940  dochcl  41941  dochvalr  41945  doch2val2  41952  dochss  41953  dochocss  41954  lclkr  42121  lclkrs  42127  lcdvbase  42181  lcdvbasess  42182  mapdunirnN  42238  aks4d1p4  42660  aks4d1p5  42661  aks4d1p7  42664  aks4d1p8  42668  sticksstones1  42727  aks6d1c6lem2  42752  grpods  42775  unitscyglem1  42776  unitscyglem2  42777  unitscyglem4  42779  mhpind  43140  mhphf  43143  prjcrv0  43179  infdesc  43189  mzpindd  43291  fiphp3d  43360  rencldnfilem  43361  irrapx1  43369  pellexlem3  43372  pellfundre  43422  pellfundge  43423  pellfundlb  43425  pellfundglb  43426  jm2.22  43536  jm2.23  43537  rpnnen3  43573  pwssplit4  43630  pwfi2f1o  43637  hbtlem6  43670  dgraalem  43686  dgraaub  43689  itgocn  43705  onintunirab  43768  nadd2rabord  43926  nadd1rabord  43930  rfovcnvf1od  44544  fsovfd  44552  fsovcnvlem  44553  binomcxplemdvbinom  44893  binomcxplemcvg  44894  binomcxplemnotnn0  44896  uzwo4  45597  disjf1o  45733  icof  45759  allbutfiinf  45958  supminfxr  46002  supminfxr2  46007  fsumsupp0  46118  sumnnodd  46170  fnlimabslt  46217  liminfvalxr  46321  ioodvbdlimc1lem1  46469  dvnprodlem1  46484  dvnprodlem2  46485  stoweidlem14  46552  stoweidlem34  46572  stoweidlem44  46582  stoweidlem50  46588  stoweidlem51  46589  stoweidlem52  46590  stoweidlem57  46595  stoweidlem59  46597  fourierdlem19  46664  fourierdlem20  46665  fourierdlem25  46670  fourierdlem31  46676  fourierdlem37  46682  fourierdlem42  46687  fourierdlem51  46695  fourierdlem54  46698  fourierdlem64  46708  fourierdlem79  46723  elaa2lem  46771  etransclem16  46788  etransclem24  46796  etransclem31  46803  etransclem33  46805  etransclem34  46806  etransclem48  46820  salgencl  46870  salexct  46872  salgenuni  46875  subsaliuncllem  46895  meadjiunlem  47003  caragenss  47042  caratheodory  47066  ovnlecvr  47096  ovnlerp  47100  ovn0lem  47103  ovnsubaddlem1  47108  hoidmv1lelem1  47129  hoidmv1lelem3  47131  hoidmvlelem1  47133  hoidmvlelem2  47134  hoidmvlelem3  47135  hoidmvlelem4  47136  ovnhoilem1  47139  ovnhoilem2  47140  ovnlecvr2  47148  ovncvr2  47149  opnvonmbllem2  47171  ovolval4lem1  47187  pimconstlt1  47240  pimgtmnf2  47252  pimdecfgtioc  47253  pimincfltioc  47254  pimdecfgtioo  47255  pimincfltioo  47256  sssmf  47276  incsmflem  47279  smfaddlem1  47301  smfaddlem2  47302  decsmflem  47304  smflimlem1  47309  smflimlem2  47310  smflimlem3  47311  smfrec  47327  smfmullem4  47332  smfdiv  47335  smfsuplem1  47349  smfsuplem3  47351  smfinflem  47355  smflimsuplem1  47358  smflimsuplem7  47364  smfliminflem  47368  sprsymrelfolem1  48062  prmdvdsfmtnof1lem1  48157  prmdvdsfmtnof  48159  perfectALTVlem2  48308  isubgredg  48452  isubgruhgr  48454  isubgrgrim  48515  uhgrimisgrgric  48517  uspgrlimlem1  48574  uspgrlimlem4  48577  uspgrlim  48578  grlimgrtrilem2  48588  oddibas  48759  2zlidl  48826  2zrngbas  48828  2zrng0  48830  isclatd  49568  topclat  49583