Theorem ssrab2 4009

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

Syntax hints:  {crab 3067   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  ssrab3  4011  ssrabeq  4013  iinrab2  4995  riinrab  5009  rabexg  5250  pwnss  5267  rabelpw  5270  frminex  5560  wereu2  5577  frpomin  6228  frpoinsg  6231  wfisgOLD  6242  ssimaex  6835  f1oresrab  6981  weniso  7205  canth  7209  riotacl  7230  riotassuni  7253  onminesb  7620  onminsb  7621  onintrab  7623  onnminsb  7626  onminex  7629  tfis  7676  suppssdm  7964  fnsuppres  7978  oeeulem  8394  nnawordex  8430  pmvalg  8584  fineqvlem  8966  ordtypelem3  9209  ordtypelem4  9210  ordtypelem6  9212  hartogs  9233  card2on  9243  wdom2d  9269  oemapvali  9372  frinsg  9440  tz9.12lem1  9476  tz9.12lem3  9478  rankf  9483  cardf2  9632  cardid2  9642  cardmin2  9688  acni3  9734  dfac2a  9816  cofsmo  9956  coftr  9960  fin2i2  10005  isfin2-2  10006  enfin2i  10008  fin1a2lem11  10097  fin1a2lem12  10098  axdc3lem4  10140  ac6  10167  ondomon  10250  alephval2  10259  pwfseqlem1  10345  pwfseqlem3  10347  wunccl  10431  tskmcl  10528  infm3  11864  uzf  12514  nnwos  12584  supminf  12604  zsupss  12606  rpnnen1lem1  12647  rpnnen1lem3  12648  rpnnen1lem5  12650  ixxf  13018  fzf  13172  flval3  13463  rabssnn0fi  13634  expge0  13747  expge1  13748  hashbclem  14092  sqrlem3  14884  rlimrege0  15216  incexc2  15478  bitsf  16062  bitsfzolem  16069  sadadd2lem  16094  sadadd3  16096  sadcl  16097  smupf  16113  smuval2  16117  smupvallem  16118  smucl  16119  smueqlem  16125  lcmcllem  16229  lcmn0cl  16230  lcmledvds  16232  lcmfval  16254  lcmfcllem  16258  lcmfn0cl  16259  lcmfledvds  16265  phicl2  16397  phibnd  16400  hashdvds  16404  phiprmpw  16405  phimullem  16408  eulerth  16412  phisum  16419  odzcllem  16421  odzdvds  16424  prmreclem1  16545  prmreclem2  16546  prmreclem3  16547  prmreclem4  16548  prmreclem5  16549  hashbccl  16632  prmgaplem3  16682  prmgaplem4  16683  prdsds  17092  mrcflem  17232  isacs1i  17283  wunnat  17588  wunnatOLD  17589  dmcoass  17697  lublecl  17994  lubid  17995  issubmd  18360  mhmeql  18379  cntzval  18842  cntzssv  18849  symgsssg  18990  symgfisg  18991  pmtrdifellem4  19002  odfval  19055  odlem1  19058  odlem2  19062  odngen  19097  gexlem1  19099  gexlem2  19102  sylow2alem2  19138  sylow2blem3  19142  oddvdssubg  19371  cyggex2  19413  ablfaclem3  19605  lssacs  20144  lspf  20151  ocvfval  20783  ocvval  20784  dsmmval2  20853  dsmmsubg  20860  asplss  20988  aspsubrg  20990  psrass1lemOLD  21053  psrass1lem  21056  psrdi  21085  psrdir  21086  psrass23l  21087  psrass23  21089  resspsrmul  21096  mplbas  21108  mplsubglem  21115  mplsubrglem  21120  mplmonmul  21147  psropprmul  21319  scmatlss  21582  smadiadet  21727  pmatcoe1fsupp  21758  cpmatsubgpmat  21777  fctop  22062  cctop  22064  ppttop  22065  epttop  22067  clscld  22106  neips  22172  neiptopnei  22191  ordtbaslem  22247  ordtuni  22249  ordtcld1  22256  ordtcld2  22257  cnpfval  22293  iscnp2  22298  cmpcov2  22449  cmpsublem  22458  tgcmp  22460  conncompcld  22493  1stcfb  22504  2ndc1stc  22510  2ndcdisj  22515  finlocfin  22579  kgentopon  22597  xkotf  22644  txkgen  22711  xkococnlem  22718  imastopn  22779  kqffn  22784  opnfbas  22901  flimfnfcls  23087  alexsubALT  23110  ptcmplem2  23112  symgtgp  23165  tgpconncompeqg  23171  tgpconncomp  23172  ghmcnp  23174  tsmsfbas  23187  eltsms  23192  utoptop  23294  utopbas  23295  blfvalps  23444  blfps  23467  blf  23468  nmoffn  23781  nmofval  23784  nmogelb  23786  nmolb  23787  nmof  23789  ishtpy  24041  clsocv  24319  rrxnm  24460  rrxbasefi  24479  minveclem3b  24497  minveclem4  24501  ovolcl  24547  ovollb  24548  ovolgelb  24549  ovolge0  24550  ovolshftlem1  24578  ovolshft  24580  ovolscalem1  24582  ovolscalem2  24583  ovolsca  24584  ovolicc2lem3  24588  shftmbl  24607  iundisj  24617  dyadmax  24667  dyadmbllem  24668  opnmbllem  24670  mdegmullem  25148  uc1pval  25209  mon1pval  25211  elqaalem1  25384  elqaalem3  25386  aannenlem2  25394  aalioulem2  25398  radcnvcl  25481  radcnvlt1  25482  radcnvle  25484  ftalem4  26130  ftalem5  26131  efnnfsumcl  26157  isppw  26168  sgmval2  26197  efchtdvds  26213  sqff1o  26236  fsumdvdsdiaglem  26237  fsumdvdsdiag  26238  fsumdvdscom  26239  musum  26245  muinv  26247  sgmmul  26254  ppiub  26257  vmasum  26269  logfac2  26270  perfectlem2  26283  lgsfcl  26358  lgscl  26364  lgsquadlem1  26433  lgsquadlem2  26434  rpvmasumlem  26540  mudivsum  26583  mulogsum  26585  mulog2sumlem2  26588  vmalogdivsum2  26591  logsqvma  26595  logsqvma2  26596  selberglem3  26600  selberg  26601  selberg34r  26624  pntsval2  26629  pntrlog2bndlem1  26630  tglnunirn  26813  tglnssp  26817  incistruhgr  27352  upgrss  27361  upgrn0  27362  upgruhgr  27375  usgrss  27447  uspgrushgr  27448  ushgredgedg  27499  ushgredgedgloop  27501  vtxdun  27751  vtxdginducedm1  27813  wlknwwlksnbij  28154  hashwwlksnext  28180  frcond3  28534  numclwlk1lem2  28635  ocsh  29546  spancl  29599  shsval2i  29650  ococin  29671  chsupid  29675  speccl  30162  hatomistici  30625  chpssati  30626  iundisjf  30829  aciunf1  30902  fpwrelmap  30970  iundisjfi  31019  pwrssmgc  31180  cycpmco2f1  31293  cycpmco2rn  31294  cycpmco2lem1  31295  cycpmco2lem2  31296  cycpmco2lem3  31297  cycpmco2lem4  31298  cycpmco2lem5  31299  cycpmco2lem6  31300  cycpmco2lem7  31301  cycpmco2  31302  nsgmgclem  31498  locfinreflem  31692  zarclsiin  31723  zarcls  31726  zartopn  31727  esumrnmpt2  31936  esumpinfval  31941  sigagensiga  32009  ldgenpisyslem1  32031  ldgenpisys  32034  measvuni  32082  imambfm  32129  dya2iocuni  32150  omscl  32162  oms0  32164  omsmon  32165  omssubadd  32167  carsgcl  32171  oddpwdc  32221  eulerpartlem1  32234  eulerpartlemt  32238  eulerpartgbij  32239  eulerpartlemmf  32242  eulerpartlemgh  32245  eulerpartlemgs2  32247  ballotlem2  32355  ballotlemfc0  32359  ballotlemfcc  32360  ballotlemfmpn  32361  ballotlemiex  32368  ballotlemsup  32371  ballotlem7  32402  ballotth  32404  reprpmtf1o  32506  breprexplema  32510  hgt750lema  32537  bnj110  32738  bnj1204  32892  bnj1311  32904  fnrelpredd  32961  subfacp1lem6  33047  erdszelem2  33054  connpconn  33097  cvmliftmolem2  33144  cvmliftlem15  33160  cvmlift2lem12  33176  snmlff  33191  satfrnmapom  33232  tfisg  33692  sltval2  33786  conway  33920  eqscut2  33927  scutun12  33931  scutbdaybnd  33936  scutbdaybnd2  33937  scutbdaylt  33939  bday1s  33952  madef  33967  leftssold  33988  rightssold  33989  madebdaylemlrcut  34006  cofcut1  34017  cofcutr  34019  rankeq1o  34400  finminlem  34434  fnessref  34473  neibastop1  34475  neibastop2lem  34476  bj-rabtr  35045  bj-rabtrAUTO  35047  bj-vecssmod  35379  icoreresf  35450  phpreu  35688  fin2so  35691  poimirlem26  35730  poimirlem31  35735  poimirlem32  35736  opnmbllem0  35740  mblfinlem1  35741  mblfinlem2  35742  ismblfin  35745  mbfposadd  35751  cnambfre  35752  cover2  35799  indexa  35818  fdc  35830  sstotbnd2  35859  sstotbnd3  35861  igenidl  36148  prnc  36152  toycom  36914  lkrlss  37036  atlatmstc  37260  atlatle  37261  glbconN  37318  linepsubN  37693  pmapssat  37700  pmaple  37702  pmapsub  37709  paddssat  37755  diass  38983  diaglbN  38996  diaintclN  38999  diassdvaN  39001  docaclN  39065  dibglbN  39107  dibintclN  39108  diclspsn  39135  dihglblem2N  39235  dih1dimatlem  39270  dihglb2  39283  dochval2  39293  dochcl  39294  dochvalr  39298  doch2val2  39305  dochss  39306  dochocss  39307  lclkr  39474  lclkrs  39480  lcdvbase  39534  lcdvbasess  39535  mapdunirnN  39591  aks4d1p4  40015  aks4d1p5  40016  aks4d1p7  40019  aks4d1p8  40023  sticksstones1  40030  mhpind  40206  infdesc  40396  mzpindd  40484  fiphp3d  40557  rencldnfilem  40558  irrapx1  40566  pellexlem3  40569  pellfundre  40619  pellfundge  40620  pellfundlb  40622  pellfundglb  40623  jm2.22  40733  jm2.23  40734  rpnnen3  40770  pwssplit4  40830  pwfi2f1o  40837  hbtlem6  40870  dgraalem  40886  dgraaub  40889  itgocn  40905  rgspncl  40910  rfovcnvf1od  41501  fsovfd  41509  fsovcnvlem  41510  binomcxplemdvbinom  41860  binomcxplemcvg  41861  binomcxplemnotnn0  41863  uzwo4  42490  disjf1o  42618  icof  42648  allbutfiinf  42850  supminfxr  42894  supminfxr2  42899  fsumsupp0  43009  sumnnodd  43061  fnlimabslt  43110  liminfvalxr  43214  ioodvbdlimc1lem1  43362  dvnprodlem1  43377  dvnprodlem2  43378  stoweidlem14  43445  stoweidlem34  43465  stoweidlem44  43475  stoweidlem50  43481  stoweidlem51  43482  stoweidlem52  43483  stoweidlem57  43488  stoweidlem59  43490  fourierdlem19  43557  fourierdlem20  43558  fourierdlem25  43563  fourierdlem31  43569  fourierdlem37  43575  fourierdlem42  43580  fourierdlem51  43588  fourierdlem54  43591  fourierdlem64  43601  fourierdlem79  43616  elaa2lem  43664  etransclem16  43681  etransclem24  43689  etransclem31  43696  etransclem33  43698  etransclem34  43699  etransclem48  43713  salgencl  43761  salexct  43763  salgenuni  43766  subsaliuncllem  43786  meadjiunlem  43893  caragenss  43932  caratheodory  43956  ovnlecvr  43986  ovnsslelem  43988  ovnlerp  43990  ovn0lem  43993  ovnsubaddlem1  43998  hoidmv1lelem1  44019  hoidmv1lelem3  44021  hoidmvlelem1  44023  hoidmvlelem2  44024  hoidmvlelem3  44025  hoidmvlelem4  44026  ovnhoilem1  44029  ovnhoilem2  44030  ovnlecvr2  44038  ovncvr2  44039  opnvonmbllem2  44061  ovolval4lem1  44077  ovolval5lem3  44082  pimconstlt1  44129  pimltpnf  44130  pimiooltgt  44135  pimgtmnf2  44138  pimdecfgtioc  44139  pimincfltioc  44140  pimdecfgtioo  44141  pimincfltioo  44142  sssmf  44161  incsmflem  44164  smfaddlem1  44185  smfaddlem2  44186  decsmflem  44188  smflimlem1  44193  smflimlem2  44194  smflimlem3  44195  smfrec  44210  smfmullem4  44215  smfdiv  44218  smfsuplem1  44231  smfsuplem3  44233  smfinflem  44237  smflimsuplem1  44240  smflimsuplem7  44246  smfliminflem  44250  sprsymrelfolem1  44832  prmdvdsfmtnof1lem1  44924  prmdvdsfmtnof  44926  perfectALTVlem2  45062  rabsubmgmd  45233  mgmhmeql  45245  oddibas  45255  2zlidl  45380  2zrngbas  45382  2zrng0  45384  isclatd  46157  topclat  46172