Theorem ssrab2 4008

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

This proof depends on syntax axioms:  {crab 3416   ⊆ wss 3900

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-ss 3901

This theorem is used by:  ssrab3  4010  ssrabeq  4012  iinrab2  5033  riinrab  5049  rabelpw  5305  frminex  5637  wereu2  5655  predres  6368  frpomin  6369  frpoinsg  6372  ssimaex  7001  f1oresrab  7160  weniso  7395  canth  7405  riotacl  7425  riotassuni  7448  onminesb  7841  onminsb  7842  onintrab  7844  onnminsb  7847  onminex  7850  tfisg  7899  tfis  7900  suppssdm  8232  fnsuppres  8246  oeeulem  8648  nnawordex  8684  pmvalg  8895  fineqvlem  9295  ordtypelem3  9551  ordtypelem4  9552  ordtypelem6  9554  hartogs  9575  card2on  9585  wdom2d  9611  oemapvali  9722  frinsg  9792  tz9.12lem1  9831  tz9.12lem3  9833  rankf  9839  cardf2  10061  cardid2  10071  cardmin2  10119  acni3  10165  dfac2a  10247  cofsmo  10386  coftr  10390  fin2i2  10435  isfin2-2  10436  enfin2i  10438  fin1a2lem11  10527  fin1a2lem12  10528  axdc3lem4  10570  ac6  10597  ondomon  10686  alephval2  10696  pwfseqlem1  10782  pwfseqlem3  10784  wunccl  10868  tskmcl  10965  infm3  12316  uzf  13008  nnwos  13082  supminf  13102  zsupss  13104  rpnnen1lem1  13146  rpnnen1lem3  13147  rpnnen1lem5  13149  ixxf  13526  fzf  13683  flval3  13995  rabssnn0fi  14169  expge0  14281  expge1  14282  hashbclem  14638  01sqrexlem3  15454  rlimrege0  15790  incexc2  16051  bitsf  16641  bitsfzolem  16648  sadadd2lem  16673  sadadd3  16675  sadcl  16676  smupf  16692  smuval2  16696  smupvallem  16697  smucl  16698  smueqlem  16704  lcmcllem  16815  lcmn0cl  16816  lcmledvds  16818  lcmfval  16840  lcmfcllem  16844  lcmfn0cl  16845  lcmfledvds  16851  phicl2  16989  phibnd  16992  hashdvds  16996  phiprmpw  16997  phimullem  17000  eulerth  17004  phisum  17012  odzcllem  17014  odzdvds  17017  prmreclem1  17138  prmreclem3  17140  prmreclem4  17141  prmreclem5  17142  hashbccl  17225  prmgaplem3  17275  prmgaplem4  17276  prdsds  17685  mrcflem  17830  isacs1i  17881  wunnat  18184  dmcoass  18291  lublecl  18583  lubid  18584  rabsubmgmd  18943  mgmhmeql  18955  issubmd  19051  mhmeql  19072  cntzval  19586  cntzssv  19593  symgsssg  19732  symgfisg  19733  pmtrdifellem4  19744  odfval  19797  odlem1  19800  odlem2  19804  odngen  19842  gexlem1  19844  gexlem2  19847  sylow2alem2  19883  sylow2blem3  19887  oddvdssubg  20120  cyggex2  20162  ablfaclem3  20354  rgspncl  20916  lssacs  21293  lspf  21300  ocvfval  22027  ocvval  22028  dsmmval2  22097  dsmmsubg  22104  asplss  22236  aspsubrg  22238  psrass1lem  22296  psrdi  22327  psrdir  22328  psrass23l  22329  psrass23  22331  resspsrmul  22338  mplbas  22352  mplsubglem  22361  mplsubrglem  22366  mplmonmul  22400  psropprmul  22610  scmatlss  22895  smadiadet  23040  pmatcoe1fsupp  23074  cpmatsubgpmat  23093  fctop  23377  cctop  23379  ppttop  23380  epttop  23382  clscld  23420  neips  23486  neiptopnei  23505  ordtbaslem  23561  ordtuni  23563  ordtcld1  23570  ordtcld2  23571  cnpfval  23607  iscnp2  23612  cmpcov2  23763  cmpsublem  23772  tgcmp  23774  conncompcld  23807  1stcfb  23818  2ndc1stc  23824  2ndcdisj  23830  finlocfin  23894  kgentopon  23912  xkotf  23959  txkgen  24026  xkococnlem  24033  imastopn  24094  kqffn  24099  opnfbas  24216  flimfnfcls  24402  alexsubALT  24425  ptcmplem2  24427  symgtgp  24480  tgpconncompeqg  24486  tgpconncomp  24487  ghmcnp  24489  tsmsfbas  24502  eltsms  24507  utoptop  24608  utopbas  24609  blfvalps  24757  blfps  24780  blf  24781  nmoffn  25085  nmofval  25088  nmogelb  25090  nmolb  25091  nmof  25093  ishtpy  25348  clsocv  25626  rrxnm  25767  rrxbasefi  25786  minveclem3b  25804  minveclem4  25808  ovolcl  25854  ovollb  25855  ovolgelb  25856  ovolge0  25857  ovolshftlem1  25885  ovolshft  25887  ovolscalem1  25889  ovolscalem2  25890  ovolsca  25891  ovolicc2lem3  25895  shftmbl  25914  iundisj  25924  dyadmax  25974  dyadmbllem  25975  opnmbllem  25977  mdegmullem  26451  uc1pval  26513  mon1pval  26515  elqaalem1  26699  elqaalem3  26701  aannenlem2  26713  aalioulem2  26717  radcnvcl  26801  radcnvlt1  26802  radcnvle  26804  ftalem4  27460  ftalem5  27461  efnnfsumcl  27487  isppw  27498  sgmval2  27527  efchtdvds  27543  sqff1o  27566  fsumdvdsdiaglem  27567  fsumdvdsdiag  27568  fsumdvdscom  27569  musum  27575  muinv  27577  sgmmul  27585  ppiub  27588  vmasum  27600  logfac2  27601  perfectlem2  27614  lgsfcl  27689  lgscl  27695  lgsquadlem1  27764  lgsquadlem2  27765  rpvmasumlem  27871  mudivsum  27914  mulogsum  27916  mulog2sumlem2  27919  vmalogdivsum2  27922  logsqvma  27926  logsqvma2  27927  selberglem3  27931  selberg  27932  selberg34r  27955  pntsval2  27960  pntrlog2bndlem1  27961  infdesc  28024  ltsval2  28070  conway  28222  eqcuts2  28229  cutsun12  28233  cutbdaybnd  28238  cutbdaybnd2  28239  cutbdaylt  28241  bday1  28257  cuteq0  28258  madef  28279  leftssold  28314  rightssold  28315  madebdaylemlrcut  28342  sltsbday  28360  cofcut1  28363  cofcutr  28367  cutlt  28375  precsexlem8  28657  precsexlem11  28660  onssno  28697  oncutlt  28707  oniso  28714  bdayons  28719  bdayn0p1  28812  tglnunirn  29068  tglnssp  29072  plngrnssp  29314  plngssp  29316  incistruhgr  29714  upgrss  29723  upgrn0  29724  upgruhgr  29737  usgrss  29812  uspgrushgr  29815  ushgredgedg  29867  ushgredgedgloop  29869  vtxdun  30119  vtxdginducedm1  30181  wlknwwlksnbij  30534  hashwwlksnext  30560  frcond3  30927  numclwlk1lem2  31028  ocsh  31942  spancl  31995  shsval2i  32046  ococin  32067  chsupid  32071  speccl  32558  hatomistici  33021  chpssati  33022  iundisjf  33281  aciunf1  33355  fpwrelmap  33421  iundisjfi  33484  pwrssmgc  33660  cycpmco2f1  33784  cycpmco2rn  33785  cycpmco2lem1  33786  cycpmco2lem2  33787  cycpmco2lem3  33788  cycpmco2lem4  33789  cycpmco2lem5  33790  cycpmco2lem6  33791  cycpmco2lem7  33792  cycpmco2  33793  fxpss  33826  nsgmgclem  34066  0mplrim  34257  selvply1rhmlemb  34262  selvply1rhm0  34269  extvfvcl  34279  mplmulmvr  34282  evlextv  34285  mplvrpmlem  34286  mplvrpmga  34288  mplvrpmrhm  34290  psrmonmul  34293  esplylem  34309  esplympl  34310  esplymhp  34311  esplyfv1  34312  esplyfv  34313  esplyfval3  34315  esplyfval1  34316  esplyfvaln  34317  constrsuc  34481  locfinreflem  34583  zarclsiin  34614  zarcls  34617  zartopn  34618  esumrnmpt2  34811  esumpinfval  34816  sigagensiga  34885  ldgenpisyslem1  34907  ldgenpisys  34910  measvuni  34958  imambfm  35005  dya2iocuni  35026  omscl  35038  oms0  35040  omsmon  35041  omssubadd  35043  carsgcl  35047  oddpwdc  35097  eulerpartlem1  35110  eulerpartlemt  35114  eulerpartgbij  35115  eulerpartlemmf  35118  eulerpartlemgh  35121  eulerpartlemgs2  35123  ballotlem2  35232  ballotlemfc0  35236  ballotlemfcc  35237  ballotlemfmpn  35238  ballotlemiex  35245  ballotlemsup  35248  ballotlem7  35279  ballotth  35281  reprpmtf1o  35366  breprexplema  35370  hgt750lema  35397  bnj110  35599  bnj1204  35753  bnj1311  35765  fnrelpredd  35845  subfacp1lem6  36158  erdszelem2  36165  connpconn  36208  cvmliftmolem2  36255  cvmliftlem15  36271  cvmlift2lem12  36287  snmlff  36302  satfrnmapom  36343  rankeq1o  37147  nmuladdel  37176  finminlem  37321  fnessref  37360  neibastop1  37362  neibastop2lem  37363  weiunlem  37466  weiunse  37471  bj-rabtr  38058  bj-rabtrAUTO  38060  bj-vecssmod  38470  icoreresf  38543  phpreu  38795  fin2so  38798  poimirlem26  38832  poimirlem31  38837  poimirlem32  38838  opnmbllem0  38842  mblfinlem1  38843  mblfinlem2  38844  ismblfin  38847  mbfposadd  38853  cnambfre  38854  cover2  38917  indexa  38935  fdc  38945  sstotbnd2  38974  sstotbnd3  38976  igenidl  39263  prnc  39267  toycom  40296  lkrlss  40418  atlatmstc  40642  atlatle  40643  glbconN  40700  linepsubN  41075  pmapssat  41082  pmaple  41084  pmapsub  41091  paddssat  41137  diass  42365  diaglbN  42378  diaintclN  42381  diassdvaN  42383  docaclN  42447  dibglbN  42489  dibintclN  42490  diclspsn  42517  dihglblem2N  42617  dih1dimatlem  42652  dihglb2  42665  dochval2  42675  dochcl  42676  dochvalr  42680  doch2val2  42687  dochss  42688  dochocss  42689  lclkr  42856  lclkrs  42862  lcdvbase  42916  lcdvbasess  42917  mapdunirnN  42973  aks4d1p4  43395  aks4d1p5  43396  aks4d1p7  43399  aks4d1p8  43403  sticksstones1  43462  aks6d1c6lem2  43487  grpods  43510  unitscyglem1  43511  unitscyglem2  43512  unitscyglem4  43514  mhpind  43888  mhphf  43891  frlmnzcoordinf  43920  frlmnzcoordcl  43921  frlmnzcoordn0  43923  prjcrv0  43935  mzpindd  44023  fiphp3d  44092  rencldnfilem  44093  irrapx1  44101  pellexlem3  44104  pellfundre  44154  pellfundge  44155  pellfundlb  44157  pellfundglb  44158  jm2.22  44268  jm2.23  44269  rpnnen3  44305  pwssplit4  44357  pwfi2f1o  44364  hbtlem6  44396  dgraalem  44412  dgraaub  44415  itgocn  44431  onintunirab  44490  nadd2rabord  44648  nadd1rabord  44652  rfovcnvf1od  45265  fsovfd  45273  fsovcnvlem  45274  binomcxplemdvbinom  45598  binomcxplemcvg  45599  binomcxplemnotnn0  45601  uzwo4  46344  disjf1o  46479  icof  46505  allbutfiinf  46703  supminfxr  46747  supminfxr2  46752  fsumsupp0  46863  sumnnodd  46915  fnlimabslt  46962  liminfvalxr  47066  ioodvbdlimc1lem1  47214  dvnprodlem1  47229  dvnprodlem2  47230  stoweidlem14  47297  stoweidlem34  47317  stoweidlem44  47327  stoweidlem50  47333  stoweidlem51  47334  stoweidlem52  47335  stoweidlem57  47340  stoweidlem59  47342  fourierdlem19  47409  fourierdlem20  47410  fourierdlem25  47415  fourierdlem31  47421  fourierdlem37  47427  fourierdlem42  47432  fourierdlem51  47440  fourierdlem54  47443  fourierdlem64  47453  fourierdlem79  47468  elaa2lem  47516  etransclem16  47533  etransclem24  47541  etransclem31  47548  etransclem33  47550  etransclem34  47551  etransclem48  47565  salgencl  47615  salexct  47617  salgenuni  47620  subsaliuncllem  47640  meadjiunlem  47748  caragenss  47787  caratheodory  47811  ovnlecvr  47841  ovnlerp  47845  ovn0lem  47848  ovnsubaddlem1  47853  hoidmv1lelem1  47874  hoidmv1lelem3  47876  hoidmvlelem1  47878  hoidmvlelem2  47879  hoidmvlelem3  47880  hoidmvlelem4  47881  ovnhoilem1  47884  ovnhoilem2  47885  ovnlecvr2  47893  ovncvr2  47894  opnvonmbllem2  47916  ovolval4lem1  47932  pimconstlt1  47985  pimgtmnf2  47997  pimdecfgtioc  47998  pimincfltioc  47999  pimdecfgtioo  48000  pimincfltioo  48001  sssmf  48021  incsmflem  48024  smfaddlem1  48046  smfaddlem2  48047  decsmflem  48049  smflimlem1  48054  smflimlem2  48055  smflimlem3  48056  smfrec  48072  smfmullem4  48077  smfdiv  48080  smfpimcclem  48090  smfsuplem1  48094  smfsuplem3  48096  smfinflem  48100  smflimsuplem1  48103  smflimsuplem7  48109  smfliminflem  48113  tmachlem-agreeself  48219  tmachlem-agreeprod  48220  tmachlem-uassst  48226  tmachlem-extpcover  48228  tmachlem-agreefin  48231  sprsymrelfolem1  48847  prmdvdsfmtnof1lem1  48942  prmdvdsfmtnof  48944  perfectALTVlem2  49093  isubgredg  49237  isubgruhgr  49239  isubgrgrim  49300  uhgrimisgrgric  49302  uspgrlimlem1  49359  uspgrlimlem4  49362  uspgrlim  49363  grlimgrtrilem2  49373  oddibas  49543  2zlidl  49610  2zrngbas  49612  2zrng0  49614  isclatd  50428  topclat  50443  dvsec  51284  dvcsc  51285  dvcot  51286