Theorem ssrab2 4077

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

Syntax hints:  {crab 3433   ⊆ wss 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-in 3955  df-ss 3965

This theorem is referenced by:  ssrab3  4080  ssrabeq  4082  iinrab2  5073  riinrab  5087  rabexg  5331  pwnss  5349  rabelpw  5352  frminex  5656  wereu2  5673  predres  6338  frpomin  6339  frpoinsg  6342  wfisgOLD  6353  ssimaex  6974  f1oresrab  7122  weniso  7348  canth  7359  riotacl  7380  riotassuni  7403  onminesb  7778  onminsb  7779  onintrab  7781  onnminsb  7784  onminex  7787  tfisg  7840  tfis  7841  suppssdm  8159  fnsuppres  8173  oeeulem  8598  nnawordex  8634  pmvalg  8828  fineqvlem  9259  ordtypelem3  9512  ordtypelem4  9513  ordtypelem6  9515  hartogs  9536  card2on  9546  wdom2d  9572  oemapvali  9676  frinsg  9743  tz9.12lem1  9779  tz9.12lem3  9781  rankf  9786  cardf2  9935  cardid2  9945  cardmin2  9991  acni3  10039  dfac2a  10121  cofsmo  10261  coftr  10265  fin2i2  10310  isfin2-2  10311  enfin2i  10313  fin1a2lem11  10402  fin1a2lem12  10403  axdc3lem4  10445  ac6  10472  ondomon  10555  alephval2  10564  pwfseqlem1  10650  pwfseqlem3  10652  wunccl  10736  tskmcl  10833  infm3  12170  uzf  12822  nnwos  12896  supminf  12916  zsupss  12918  rpnnen1lem1  12959  rpnnen1lem3  12960  rpnnen1lem5  12962  ixxf  13331  fzf  13485  flval3  13777  rabssnn0fi  13948  expge0  14061  expge1  14062  hashbclem  14408  01sqrexlem3  15188  rlimrege0  15520  incexc2  15781  bitsf  16365  bitsfzolem  16372  sadadd2lem  16397  sadadd3  16399  sadcl  16400  smupf  16416  smuval2  16420  smupvallem  16421  smucl  16422  smueqlem  16428  lcmcllem  16530  lcmn0cl  16531  lcmledvds  16533  lcmfval  16555  lcmfcllem  16559  lcmfn0cl  16560  lcmfledvds  16566  phicl2  16698  phibnd  16701  hashdvds  16705  phiprmpw  16706  phimullem  16709  eulerth  16713  phisum  16720  odzcllem  16722  odzdvds  16725  prmreclem1  16846  prmreclem2  16847  prmreclem3  16848  prmreclem4  16849  prmreclem5  16850  hashbccl  16933  prmgaplem3  16983  prmgaplem4  16984  prdsds  17407  mrcflem  17547  isacs1i  17598  wunnat  17904  wunnatOLD  17905  dmcoass  18013  lublecl  18311  lubid  18312  issubmd  18684  mhmeql  18704  cntzval  19180  cntzssv  19187  symgsssg  19330  symgfisg  19331  pmtrdifellem4  19342  odfval  19395  odlem1  19398  odlem2  19402  odngen  19440  gexlem1  19442  gexlem2  19445  sylow2alem2  19481  sylow2blem3  19485  oddvdssubg  19718  cyggex2  19760  ablfaclem3  19952  lssacs  20571  lspf  20578  ocvfval  21211  ocvval  21212  dsmmval2  21283  dsmmsubg  21290  asplss  21420  aspsubrg  21422  psrass1lemOLD  21485  psrass1lem  21488  psrdi  21518  psrdir  21519  psrass23l  21520  psrass23  21522  resspsrmul  21529  mplbas  21541  mplsubglem  21550  mplsubrglem  21555  mplmonmul  21583  psropprmul  21752  scmatlss  22019  smadiadet  22164  pmatcoe1fsupp  22195  cpmatsubgpmat  22214  fctop  22499  cctop  22501  ppttop  22502  epttop  22504  clscld  22543  neips  22609  neiptopnei  22628  ordtbaslem  22684  ordtuni  22686  ordtcld1  22693  ordtcld2  22694  cnpfval  22730  iscnp2  22735  cmpcov2  22886  cmpsublem  22895  tgcmp  22897  conncompcld  22930  1stcfb  22941  2ndc1stc  22947  2ndcdisj  22952  finlocfin  23016  kgentopon  23034  xkotf  23081  txkgen  23148  xkococnlem  23155  imastopn  23216  kqffn  23221  opnfbas  23338  flimfnfcls  23524  alexsubALT  23547  ptcmplem2  23549  symgtgp  23602  tgpconncompeqg  23608  tgpconncomp  23609  ghmcnp  23611  tsmsfbas  23624  eltsms  23629  utoptop  23731  utopbas  23732  blfvalps  23881  blfps  23904  blf  23905  nmoffn  24220  nmofval  24223  nmogelb  24225  nmolb  24226  nmof  24228  ishtpy  24480  clsocv  24759  rrxnm  24900  rrxbasefi  24919  minveclem3b  24937  minveclem4  24941  ovolcl  24987  ovollb  24988  ovolgelb  24989  ovolge0  24990  ovolshftlem1  25018  ovolshft  25020  ovolscalem1  25022  ovolscalem2  25023  ovolsca  25024  ovolicc2lem3  25028  shftmbl  25047  iundisj  25057  dyadmax  25107  dyadmbllem  25108  opnmbllem  25110  mdegmullem  25588  uc1pval  25649  mon1pval  25651  elqaalem1  25824  elqaalem3  25826  aannenlem2  25834  aalioulem2  25838  radcnvcl  25921  radcnvlt1  25922  radcnvle  25924  ftalem4  26570  ftalem5  26571  efnnfsumcl  26597  isppw  26608  sgmval2  26637  efchtdvds  26653  sqff1o  26676  fsumdvdsdiaglem  26677  fsumdvdsdiag  26678  fsumdvdscom  26679  musum  26685  muinv  26687  sgmmul  26694  ppiub  26697  vmasum  26709  logfac2  26710  perfectlem2  26723  lgsfcl  26798  lgscl  26804  lgsquadlem1  26873  lgsquadlem2  26874  rpvmasumlem  26980  mudivsum  27023  mulogsum  27025  mulog2sumlem2  27028  vmalogdivsum2  27031  logsqvma  27035  logsqvma2  27036  selberglem3  27040  selberg  27041  selberg34r  27064  pntsval2  27069  pntrlog2bndlem1  27070  sltval2  27149  conway  27290  eqscut2  27297  scutun12  27301  scutbdaybnd  27306  scutbdaybnd2  27307  scutbdaylt  27309  bday1s  27322  cuteq0  27323  madef  27341  leftssold  27363  rightssold  27364  madebdaylemlrcut  27383  cofcut1  27397  cofcutr  27401  cutlt  27409  precsexlem8  27650  precsexlem11  27653  tglnunirn  27789  tglnssp  27793  incistruhgr  28329  upgrss  28338  upgrn0  28339  upgruhgr  28352  usgrss  28424  uspgrushgr  28425  ushgredgedg  28476  ushgredgedgloop  28478  vtxdun  28728  vtxdginducedm1  28790  wlknwwlksnbij  29132  hashwwlksnext  29158  frcond3  29512  numclwlk1lem2  29613  ocsh  30524  spancl  30577  shsval2i  30628  ococin  30649  chsupid  30653  speccl  31140  hatomistici  31603  chpssati  31604  iundisjf  31808  aciunf1  31876  fpwrelmap  31946  iundisjfi  31995  pwrssmgc  32158  cycpmco2f1  32271  cycpmco2rn  32272  cycpmco2lem1  32273  cycpmco2lem2  32274  cycpmco2lem3  32275  cycpmco2lem4  32276  cycpmco2lem5  32277  cycpmco2lem6  32278  cycpmco2lem7  32279  cycpmco2  32280  nsgmgclem  32511  locfinreflem  32809  zarclsiin  32840  zarcls  32843  zartopn  32844  esumrnmpt2  33055  esumpinfval  33060  sigagensiga  33128  ldgenpisyslem1  33150  ldgenpisys  33153  measvuni  33201  imambfm  33250  dya2iocuni  33271  omscl  33283  oms0  33285  omsmon  33286  omssubadd  33288  carsgcl  33292  oddpwdc  33342  eulerpartlem1  33355  eulerpartlemt  33359  eulerpartgbij  33360  eulerpartlemmf  33363  eulerpartlemgh  33366  eulerpartlemgs2  33368  ballotlem2  33476  ballotlemfc0  33480  ballotlemfcc  33481  ballotlemfmpn  33482  ballotlemiex  33489  ballotlemsup  33492  ballotlem7  33523  ballotth  33525  reprpmtf1o  33627  breprexplema  33631  hgt750lema  33658  bnj110  33858  bnj1204  34012  bnj1311  34024  fnrelpredd  34081  subfacp1lem6  34165  erdszelem2  34172  connpconn  34215  cvmliftmolem2  34262  cvmliftlem15  34278  cvmlift2lem12  34294  snmlff  34309  satfrnmapom  34350  rankeq1o  35132  finminlem  35192  fnessref  35231  neibastop1  35233  neibastop2lem  35234  bj-rabtr  35799  bj-rabtrAUTO  35801  bj-vecssmod  36151  icoreresf  36222  phpreu  36461  fin2so  36464  poimirlem26  36503  poimirlem31  36508  poimirlem32  36509  opnmbllem0  36513  mblfinlem1  36514  mblfinlem2  36515  ismblfin  36518  mbfposadd  36524  cnambfre  36525  cover2  36572  indexa  36590  fdc  36602  sstotbnd2  36631  sstotbnd3  36633  igenidl  36920  prnc  36924  toycom  37832  lkrlss  37954  atlatmstc  38178  atlatle  38179  glbconN  38236  glbconNOLD  38237  linepsubN  38612  pmapssat  38619  pmaple  38621  pmapsub  38628  paddssat  38674  diass  39902  diaglbN  39915  diaintclN  39918  diassdvaN  39920  docaclN  39984  dibglbN  40026  dibintclN  40027  diclspsn  40054  dihglblem2N  40154  dih1dimatlem  40189  dihglb2  40202  dochval2  40212  dochcl  40213  dochvalr  40217  doch2val2  40224  dochss  40225  dochocss  40226  lclkr  40393  lclkrs  40399  lcdvbase  40453  lcdvbasess  40454  mapdunirnN  40510  aks4d1p4  40933  aks4d1p5  40934  aks4d1p7  40937  aks4d1p8  40941  sticksstones1  40951  mhpind  41164  mhphf  41167  prjcrv0  41372  infdesc  41382  mzpindd  41470  fiphp3d  41543  rencldnfilem  41544  irrapx1  41552  pellexlem3  41555  pellfundre  41605  pellfundge  41606  pellfundlb  41608  pellfundglb  41609  jm2.22  41720  jm2.23  41721  rpnnen3  41757  pwssplit4  41817  pwfi2f1o  41824  hbtlem6  41857  dgraalem  41873  dgraaub  41876  itgocn  41892  rgspncl  41897  onintunirab  41962  nadd2rabord  42121  nadd1rabord  42125  rfovcnvf1od  42741  fsovfd  42749  fsovcnvlem  42750  binomcxplemdvbinom  43098  binomcxplemcvg  43099  binomcxplemnotnn0  43101  uzwo4  43726  disjf1o  43875  icof  43904  allbutfiinf  44117  supminfxr  44161  supminfxr2  44166  fsumsupp0  44281  sumnnodd  44333  fnlimabslt  44382  liminfvalxr  44486  ioodvbdlimc1lem1  44634  dvnprodlem1  44649  dvnprodlem2  44650  stoweidlem14  44717  stoweidlem34  44737  stoweidlem44  44747  stoweidlem50  44753  stoweidlem51  44754  stoweidlem52  44755  stoweidlem57  44760  stoweidlem59  44762  fourierdlem19  44829  fourierdlem20  44830  fourierdlem25  44835  fourierdlem31  44841  fourierdlem37  44847  fourierdlem42  44852  fourierdlem51  44860  fourierdlem54  44863  fourierdlem64  44873  fourierdlem79  44888  elaa2lem  44936  etransclem16  44953  etransclem24  44961  etransclem31  44968  etransclem33  44970  etransclem34  44971  etransclem48  44985  salgencl  45035  salexct  45037  salgenuni  45040  subsaliuncllem  45060  meadjiunlem  45168  caragenss  45207  caratheodory  45231  ovnlecvr  45261  ovnlerp  45265  ovn0lem  45268  ovnsubaddlem1  45273  hoidmv1lelem1  45294  hoidmv1lelem3  45296  hoidmvlelem1  45298  hoidmvlelem2  45299  hoidmvlelem3  45300  hoidmvlelem4  45301  ovnhoilem1  45304  ovnhoilem2  45305  ovnlecvr2  45313  ovncvr2  45314  opnvonmbllem2  45336  ovolval4lem1  45352  pimconstlt1  45405  pimiooltgt  45413  pimgtmnf2  45417  pimdecfgtioc  45418  pimincfltioc  45419  pimdecfgtioo  45420  pimincfltioo  45421  sssmf  45441  incsmflem  45444  smfaddlem1  45466  smfaddlem2  45467  decsmflem  45469  smflimlem1  45474  smflimlem2  45475  smflimlem3  45476  smfrec  45492  smfmullem4  45497  smfdiv  45500  smfsuplem1  45514  smfsuplem3  45516  smfinflem  45520  smflimsuplem1  45523  smflimsuplem7  45529  smfliminflem  45533  sprsymrelfolem1  46147  prmdvdsfmtnof1lem1  46239  prmdvdsfmtnof  46241  perfectALTVlem2  46377  rabsubmgmd  46548  mgmhmeql  46560  oddibas  46570  2zlidl  46786  2zrngbas  46788  2zrng0  46790  isclatd  47562  topclat  47577