Theorem ssrab2 4076

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

Syntax hints:  {crab 3433   ⊆ wss 3947

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 3954  df-ss 3964

This theorem is referenced by:  ssrab3  4079  ssrabeq  4081  iinrab2  5072  riinrab  5086  rabexg  5330  pwnss  5348  rabelpw  5351  frminex  5655  wereu2  5672  predres  6337  frpomin  6338  frpoinsg  6341  wfisgOLD  6352  ssimaex  6972  f1oresrab  7120  weniso  7346  canth  7357  riotacl  7378  riotassuni  7401  onminesb  7776  onminsb  7777  onintrab  7779  onnminsb  7782  onminex  7785  tfisg  7838  tfis  7839  suppssdm  8157  fnsuppres  8171  oeeulem  8597  nnawordex  8633  pmvalg  8827  fineqvlem  9258  ordtypelem3  9511  ordtypelem4  9512  ordtypelem6  9514  hartogs  9535  card2on  9545  wdom2d  9571  oemapvali  9675  frinsg  9742  tz9.12lem1  9778  tz9.12lem3  9780  rankf  9785  cardf2  9934  cardid2  9944  cardmin2  9990  acni3  10038  dfac2a  10120  cofsmo  10260  coftr  10264  fin2i2  10309  isfin2-2  10310  enfin2i  10312  fin1a2lem11  10401  fin1a2lem12  10402  axdc3lem4  10444  ac6  10471  ondomon  10554  alephval2  10563  pwfseqlem1  10649  pwfseqlem3  10651  wunccl  10735  tskmcl  10832  infm3  12169  uzf  12821  nnwos  12895  supminf  12915  zsupss  12917  rpnnen1lem1  12958  rpnnen1lem3  12959  rpnnen1lem5  12961  ixxf  13330  fzf  13484  flval3  13776  rabssnn0fi  13947  expge0  14060  expge1  14061  hashbclem  14407  01sqrexlem3  15187  rlimrege0  15519  incexc2  15780  bitsf  16364  bitsfzolem  16371  sadadd2lem  16396  sadadd3  16398  sadcl  16399  smupf  16415  smuval2  16419  smupvallem  16420  smucl  16421  smueqlem  16427  lcmcllem  16529  lcmn0cl  16530  lcmledvds  16532  lcmfval  16554  lcmfcllem  16558  lcmfn0cl  16559  lcmfledvds  16565  phicl2  16697  phibnd  16700  hashdvds  16704  phiprmpw  16705  phimullem  16708  eulerth  16712  phisum  16719  odzcllem  16721  odzdvds  16724  prmreclem1  16845  prmreclem2  16846  prmreclem3  16847  prmreclem4  16848  prmreclem5  16849  hashbccl  16932  prmgaplem3  16982  prmgaplem4  16983  prdsds  17406  mrcflem  17546  isacs1i  17597  wunnat  17903  wunnatOLD  17904  dmcoass  18012  lublecl  18310  lubid  18311  issubmd  18683  mhmeql  18703  cntzval  19179  cntzssv  19186  symgsssg  19328  symgfisg  19329  pmtrdifellem4  19340  odfval  19393  odlem1  19396  odlem2  19400  odngen  19438  gexlem1  19440  gexlem2  19443  sylow2alem2  19479  sylow2blem3  19483  oddvdssubg  19715  cyggex2  19757  ablfaclem3  19949  lssacs  20566  lspf  20573  ocvfval  21203  ocvval  21204  dsmmval2  21275  dsmmsubg  21282  asplss  21410  aspsubrg  21412  psrass1lemOLD  21475  psrass1lem  21478  psrdi  21508  psrdir  21509  psrass23l  21510  psrass23  21512  resspsrmul  21519  mplbas  21531  mplsubglem  21540  mplsubrglem  21545  mplmonmul  21573  psropprmul  21742  scmatlss  22009  smadiadet  22154  pmatcoe1fsupp  22185  cpmatsubgpmat  22204  fctop  22489  cctop  22491  ppttop  22492  epttop  22494  clscld  22533  neips  22599  neiptopnei  22618  ordtbaslem  22674  ordtuni  22676  ordtcld1  22683  ordtcld2  22684  cnpfval  22720  iscnp2  22725  cmpcov2  22876  cmpsublem  22885  tgcmp  22887  conncompcld  22920  1stcfb  22931  2ndc1stc  22937  2ndcdisj  22942  finlocfin  23006  kgentopon  23024  xkotf  23071  txkgen  23138  xkococnlem  23145  imastopn  23206  kqffn  23211  opnfbas  23328  flimfnfcls  23514  alexsubALT  23537  ptcmplem2  23539  symgtgp  23592  tgpconncompeqg  23598  tgpconncomp  23599  ghmcnp  23601  tsmsfbas  23614  eltsms  23619  utoptop  23721  utopbas  23722  blfvalps  23871  blfps  23894  blf  23895  nmoffn  24210  nmofval  24213  nmogelb  24215  nmolb  24216  nmof  24218  ishtpy  24470  clsocv  24749  rrxnm  24890  rrxbasefi  24909  minveclem3b  24927  minveclem4  24931  ovolcl  24977  ovollb  24978  ovolgelb  24979  ovolge0  24980  ovolshftlem1  25008  ovolshft  25010  ovolscalem1  25012  ovolscalem2  25013  ovolsca  25014  ovolicc2lem3  25018  shftmbl  25037  iundisj  25047  dyadmax  25097  dyadmbllem  25098  opnmbllem  25100  mdegmullem  25578  uc1pval  25639  mon1pval  25641  elqaalem1  25814  elqaalem3  25816  aannenlem2  25824  aalioulem2  25828  radcnvcl  25911  radcnvlt1  25912  radcnvle  25914  ftalem4  26560  ftalem5  26561  efnnfsumcl  26587  isppw  26598  sgmval2  26627  efchtdvds  26643  sqff1o  26666  fsumdvdsdiaglem  26667  fsumdvdsdiag  26668  fsumdvdscom  26669  musum  26675  muinv  26677  sgmmul  26684  ppiub  26687  vmasum  26699  logfac2  26700  perfectlem2  26713  lgsfcl  26788  lgscl  26794  lgsquadlem1  26863  lgsquadlem2  26864  rpvmasumlem  26970  mudivsum  27013  mulogsum  27015  mulog2sumlem2  27018  vmalogdivsum2  27021  logsqvma  27025  logsqvma2  27026  selberglem3  27030  selberg  27031  selberg34r  27054  pntsval2  27059  pntrlog2bndlem1  27060  sltval2  27139  conway  27280  eqscut2  27287  scutun12  27291  scutbdaybnd  27296  scutbdaybnd2  27297  scutbdaylt  27299  bday1s  27312  cuteq0  27313  madef  27331  leftssold  27353  rightssold  27354  madebdaylemlrcut  27373  cofcut1  27387  cofcutr  27391  cutlt  27399  precsexlem8  27640  precsexlem11  27643  tglnunirn  27779  tglnssp  27783  incistruhgr  28319  upgrss  28328  upgrn0  28329  upgruhgr  28342  usgrss  28414  uspgrushgr  28415  ushgredgedg  28466  ushgredgedgloop  28468  vtxdun  28718  vtxdginducedm1  28780  wlknwwlksnbij  29122  hashwwlksnext  29148  frcond3  29502  numclwlk1lem2  29603  ocsh  30514  spancl  30567  shsval2i  30618  ococin  30639  chsupid  30643  speccl  31130  hatomistici  31593  chpssati  31594  iundisjf  31798  aciunf1  31866  fpwrelmap  31936  iundisjfi  31985  pwrssmgc  32148  cycpmco2f1  32261  cycpmco2rn  32262  cycpmco2lem1  32263  cycpmco2lem2  32264  cycpmco2lem3  32265  cycpmco2lem4  32266  cycpmco2lem5  32267  cycpmco2lem6  32268  cycpmco2lem7  32269  cycpmco2  32270  nsgmgclem  32485  locfinreflem  32758  zarclsiin  32789  zarcls  32792  zartopn  32793  esumrnmpt2  33004  esumpinfval  33009  sigagensiga  33077  ldgenpisyslem1  33099  ldgenpisys  33102  measvuni  33150  imambfm  33199  dya2iocuni  33220  omscl  33232  oms0  33234  omsmon  33235  omssubadd  33237  carsgcl  33241  oddpwdc  33291  eulerpartlem1  33304  eulerpartlemt  33308  eulerpartgbij  33309  eulerpartlemmf  33312  eulerpartlemgh  33315  eulerpartlemgs2  33317  ballotlem2  33425  ballotlemfc0  33429  ballotlemfcc  33430  ballotlemfmpn  33431  ballotlemiex  33438  ballotlemsup  33441  ballotlem7  33472  ballotth  33474  reprpmtf1o  33576  breprexplema  33580  hgt750lema  33607  bnj110  33807  bnj1204  33961  bnj1311  33973  fnrelpredd  34030  subfacp1lem6  34114  erdszelem2  34121  connpconn  34164  cvmliftmolem2  34211  cvmliftlem15  34227  cvmlift2lem12  34243  snmlff  34258  satfrnmapom  34299  rankeq1o  35081  finminlem  35141  fnessref  35180  neibastop1  35182  neibastop2lem  35183  bj-rabtr  35748  bj-rabtrAUTO  35750  bj-vecssmod  36100  icoreresf  36171  phpreu  36410  fin2so  36413  poimirlem26  36452  poimirlem31  36457  poimirlem32  36458  opnmbllem0  36462  mblfinlem1  36463  mblfinlem2  36464  ismblfin  36467  mbfposadd  36473  cnambfre  36474  cover2  36521  indexa  36539  fdc  36551  sstotbnd2  36580  sstotbnd3  36582  igenidl  36869  prnc  36873  toycom  37781  lkrlss  37903  atlatmstc  38127  atlatle  38128  glbconN  38185  glbconNOLD  38186  linepsubN  38561  pmapssat  38568  pmaple  38570  pmapsub  38577  paddssat  38623  diass  39851  diaglbN  39864  diaintclN  39867  diassdvaN  39869  docaclN  39933  dibglbN  39975  dibintclN  39976  diclspsn  40003  dihglblem2N  40103  dih1dimatlem  40138  dihglb2  40151  dochval2  40161  dochcl  40162  dochvalr  40166  doch2val2  40173  dochss  40174  dochocss  40175  lclkr  40342  lclkrs  40348  lcdvbase  40402  lcdvbasess  40403  mapdunirnN  40459  aks4d1p4  40882  aks4d1p5  40883  aks4d1p7  40886  aks4d1p8  40890  sticksstones1  40900  mhpind  41116  mhphf  41119  prjcrv0  41319  infdesc  41329  mzpindd  41417  fiphp3d  41490  rencldnfilem  41491  irrapx1  41499  pellexlem3  41502  pellfundre  41552  pellfundge  41553  pellfundlb  41555  pellfundglb  41556  jm2.22  41667  jm2.23  41668  rpnnen3  41704  pwssplit4  41764  pwfi2f1o  41771  hbtlem6  41804  dgraalem  41820  dgraaub  41823  itgocn  41839  rgspncl  41844  onintunirab  41909  nadd2rabord  42068  nadd1rabord  42072  rfovcnvf1od  42688  fsovfd  42696  fsovcnvlem  42697  binomcxplemdvbinom  43045  binomcxplemcvg  43046  binomcxplemnotnn0  43048  uzwo4  43673  disjf1o  43822  icof  43851  allbutfiinf  44065  supminfxr  44109  supminfxr2  44114  fsumsupp0  44229  sumnnodd  44281  fnlimabslt  44330  liminfvalxr  44434  ioodvbdlimc1lem1  44582  dvnprodlem1  44597  dvnprodlem2  44598  stoweidlem14  44665  stoweidlem34  44685  stoweidlem44  44695  stoweidlem50  44701  stoweidlem51  44702  stoweidlem52  44703  stoweidlem57  44708  stoweidlem59  44710  fourierdlem19  44777  fourierdlem20  44778  fourierdlem25  44783  fourierdlem31  44789  fourierdlem37  44795  fourierdlem42  44800  fourierdlem51  44808  fourierdlem54  44811  fourierdlem64  44821  fourierdlem79  44836  elaa2lem  44884  etransclem16  44901  etransclem24  44909  etransclem31  44916  etransclem33  44918  etransclem34  44919  etransclem48  44933  salgencl  44983  salexct  44985  salgenuni  44988  subsaliuncllem  45008  meadjiunlem  45116  caragenss  45155  caratheodory  45179  ovnlecvr  45209  ovnlerp  45213  ovn0lem  45216  ovnsubaddlem1  45221  hoidmv1lelem1  45242  hoidmv1lelem3  45244  hoidmvlelem1  45246  hoidmvlelem2  45247  hoidmvlelem3  45248  hoidmvlelem4  45249  ovnhoilem1  45252  ovnhoilem2  45253  ovnlecvr2  45261  ovncvr2  45262  opnvonmbllem2  45284  ovolval4lem1  45300  pimconstlt1  45353  pimiooltgt  45361  pimgtmnf2  45365  pimdecfgtioc  45366  pimincfltioc  45367  pimdecfgtioo  45368  pimincfltioo  45369  sssmf  45389  incsmflem  45392  smfaddlem1  45414  smfaddlem2  45415  decsmflem  45417  smflimlem1  45422  smflimlem2  45423  smflimlem3  45424  smfrec  45440  smfmullem4  45445  smfdiv  45448  smfsuplem1  45462  smfsuplem3  45464  smfinflem  45468  smflimsuplem1  45471  smflimsuplem7  45477  smfliminflem  45481  sprsymrelfolem1  46095  prmdvdsfmtnof1lem1  46187  prmdvdsfmtnof  46189  perfectALTVlem2  46325  rabsubmgmd  46496  mgmhmeql  46508  oddibas  46518  2zlidl  46734  2zrngbas  46736  2zrng0  46738  isclatd  47510  topclat  47525