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

Syntax hints:  {crab 3396   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-ss 3922

This theorem is referenced by:  ssrab3  4035  ssrabeq  4037  iinrab2  5022  riinrab  5036  rabelpw  5278  rabexgOLD  5280  frminex  5602  wereu2  5620  predres  6291  frpomin  6292  frpoinsg  6295  ssimaex  6912  f1oresrab  7065  weniso  7295  canth  7307  riotacl  7327  riotassuni  7350  onminesb  7733  onminsb  7734  onintrab  7736  onnminsb  7739  onminex  7742  tfisg  7794  tfis  7795  suppssdm  8117  fnsuppres  8131  oeeulem  8526  nnawordex  8562  pmvalg  8771  fineqvlem  9167  ordtypelem3  9431  ordtypelem4  9432  ordtypelem6  9434  hartogs  9455  card2on  9465  wdom2d  9491  oemapvali  9599  frinsg  9666  tz9.12lem1  9702  tz9.12lem3  9704  rankf  9709  cardf2  9858  cardid2  9868  cardmin2  9914  acni3  9960  dfac2a  10043  cofsmo  10182  coftr  10186  fin2i2  10231  isfin2-2  10232  enfin2i  10234  fin1a2lem11  10323  fin1a2lem12  10324  axdc3lem4  10366  ac6  10393  ondomon  10476  alephval2  10485  pwfseqlem1  10571  pwfseqlem3  10573  wunccl  10657  tskmcl  10754  infm3  12102  uzf  12756  nnwos  12834  supminf  12854  zsupss  12856  rpnnen1lem1  12897  rpnnen1lem3  12898  rpnnen1lem5  12900  ixxf  13276  fzf  13432  flval3  13737  rabssnn0fi  13911  expge0  14023  expge1  14024  hashbclem  14377  01sqrexlem3  15169  rlimrege0  15504  incexc2  15763  bitsf  16356  bitsfzolem  16363  sadadd2lem  16388  sadadd3  16390  sadcl  16391  smupf  16407  smuval2  16411  smupvallem  16412  smucl  16413  smueqlem  16419  lcmcllem  16525  lcmn0cl  16526  lcmledvds  16528  lcmfval  16550  lcmfcllem  16554  lcmfn0cl  16555  lcmfledvds  16561  phicl2  16697  phibnd  16700  hashdvds  16704  phiprmpw  16705  phimullem  16708  eulerth  16712  phisum  16720  odzcllem  16722  odzdvds  16725  prmreclem1  16846  prmreclem2  16847  prmreclem3  16848  prmreclem4  16849  prmreclem5  16850  hashbccl  16933  prmgaplem3  16983  prmgaplem4  16984  prdsds  17386  mrcflem  17530  isacs1i  17581  wunnat  17884  dmcoass  17991  lublecl  18283  lubid  18284  rabsubmgmd  18596  mgmhmeql  18608  issubmd  18698  mhmeql  18718  cntzval  19218  cntzssv  19225  symgsssg  19364  symgfisg  19365  pmtrdifellem4  19376  odfval  19429  odlem1  19432  odlem2  19436  odngen  19474  gexlem1  19476  gexlem2  19479  sylow2alem2  19515  sylow2blem3  19519  oddvdssubg  19752  cyggex2  19794  ablfaclem3  19986  rgspncl  20516  lssacs  20888  lspf  20895  ocvfval  21591  ocvval  21592  dsmmval2  21661  dsmmsubg  21668  asplss  21799  aspsubrg  21801  psrass1lem  21857  psrdi  21890  psrdir  21891  psrass23l  21892  psrass23  21894  resspsrmul  21901  mplbas  21915  mplsubglem  21924  mplsubrglem  21929  mplmonmul  21959  psropprmul  22138  scmatlss  22428  smadiadet  22573  pmatcoe1fsupp  22604  cpmatsubgpmat  22623  fctop  22907  cctop  22909  ppttop  22910  epttop  22912  clscld  22950  neips  23016  neiptopnei  23035  ordtbaslem  23091  ordtuni  23093  ordtcld1  23100  ordtcld2  23101  cnpfval  23137  iscnp2  23142  cmpcov2  23293  cmpsublem  23302  tgcmp  23304  conncompcld  23337  1stcfb  23348  2ndc1stc  23354  2ndcdisj  23359  finlocfin  23423  kgentopon  23441  xkotf  23488  txkgen  23555  xkococnlem  23562  imastopn  23623  kqffn  23628  opnfbas  23745  flimfnfcls  23931  alexsubALT  23954  ptcmplem2  23956  symgtgp  24009  tgpconncompeqg  24015  tgpconncomp  24016  ghmcnp  24018  tsmsfbas  24031  eltsms  24036  utoptop  24138  utopbas  24139  blfvalps  24287  blfps  24310  blf  24311  nmoffn  24615  nmofval  24618  nmogelb  24620  nmolb  24621  nmof  24623  ishtpy  24887  clsocv  25166  rrxnm  25307  rrxbasefi  25326  minveclem3b  25344  minveclem4  25348  ovolcl  25395  ovollb  25396  ovolgelb  25397  ovolge0  25398  ovolshftlem1  25426  ovolshft  25428  ovolscalem1  25430  ovolscalem2  25431  ovolsca  25432  ovolicc2lem3  25436  shftmbl  25455  iundisj  25465  dyadmax  25515  dyadmbllem  25516  opnmbllem  25518  mdegmullem  25999  uc1pval  26061  mon1pval  26063  elqaalem1  26243  elqaalem3  26245  aannenlem2  26253  aalioulem2  26257  radcnvcl  26342  radcnvlt1  26343  radcnvle  26345  ftalem4  27002  ftalem5  27003  efnnfsumcl  27029  isppw  27040  sgmval2  27069  efchtdvds  27085  sqff1o  27108  fsumdvdsdiaglem  27109  fsumdvdsdiag  27110  fsumdvdscom  27111  musum  27117  muinv  27119  sgmmul  27128  ppiub  27131  vmasum  27143  logfac2  27144  perfectlem2  27157  lgsfcl  27232  lgscl  27238  lgsquadlem1  27307  lgsquadlem2  27308  rpvmasumlem  27414  mudivsum  27457  mulogsum  27459  mulog2sumlem2  27462  vmalogdivsum2  27465  logsqvma  27469  logsqvma2  27470  selberglem3  27474  selberg  27475  selberg34r  27498  pntsval2  27503  pntrlog2bndlem1  27504  sltval2  27584  conway  27728  eqscut2  27735  scutun12  27739  scutbdaybnd  27744  scutbdaybnd2  27745  scutbdaylt  27747  bday1s  27763  cuteq0  27764  madef  27784  leftssold  27811  rightssold  27812  madebdaylemlrcut  27831  cofcut1  27851  cofcutr  27855  cutlt  27863  precsexlem8  28139  precsexlem11  28142  onssno  28178  onscutlt  28188  onsiso  28192  bdayon  28196  bdayn0p1  28281  tglnunirn  28511  tglnssp  28515  incistruhgr  29042  upgrss  29051  upgrn0  29052  upgruhgr  29065  usgrss  29137  uspgrushgr  29140  ushgredgedg  29192  ushgredgedgloop  29194  vtxdun  29445  vtxdginducedm1  29507  wlknwwlksnbij  29851  hashwwlksnext  29877  frcond3  30231  numclwlk1lem2  30332  ocsh  31245  spancl  31298  shsval2i  31349  ococin  31370  chsupid  31374  speccl  31861  hatomistici  32324  chpssati  32325  iundisjf  32551  aciunf1  32620  fpwrelmap  32689  iundisjfi  32752  pwrssmgc  32955  cycpmco2f1  33079  cycpmco2rn  33080  cycpmco2lem1  33081  cycpmco2lem2  33082  cycpmco2lem3  33083  cycpmco2lem4  33084  cycpmco2lem5  33085  cycpmco2lem6  33086  cycpmco2lem7  33087  cycpmco2  33088  fxpss  33121  nsgmgclem  33358  constrsuc  33704  locfinreflem  33806  zarclsiin  33837  zarcls  33840  zartopn  33841  esumrnmpt2  34034  esumpinfval  34039  sigagensiga  34107  ldgenpisyslem1  34129  ldgenpisys  34132  measvuni  34180  imambfm  34229  dya2iocuni  34250  omscl  34262  oms0  34264  omsmon  34265  omssubadd  34267  carsgcl  34271  oddpwdc  34321  eulerpartlem1  34334  eulerpartlemt  34338  eulerpartgbij  34339  eulerpartlemmf  34342  eulerpartlemgh  34345  eulerpartlemgs2  34347  ballotlem2  34456  ballotlemfc0  34460  ballotlemfcc  34461  ballotlemfmpn  34462  ballotlemiex  34469  ballotlemsup  34472  ballotlem7  34503  ballotth  34505  reprpmtf1o  34593  breprexplema  34597  hgt750lema  34624  bnj110  34824  bnj1204  34978  bnj1311  34990  fnrelpredd  35055  subfacp1lem6  35157  erdszelem2  35164  connpconn  35207  cvmliftmolem2  35254  cvmliftlem15  35270  cvmlift2lem12  35286  snmlff  35301  satfrnmapom  35342  rankeq1o  36144  finminlem  36291  fnessref  36330  neibastop1  36332  neibastop2lem  36333  weiunlem2  36436  weiunse  36441  bj-rabtr  36903  bj-rabtrAUTO  36905  bj-vecssmod  37254  icoreresf  37325  phpreu  37583  fin2so  37586  poimirlem26  37625  poimirlem31  37630  poimirlem32  37631  opnmbllem0  37635  mblfinlem1  37636  mblfinlem2  37637  ismblfin  37640  mbfposadd  37646  cnambfre  37647  cover2  37694  indexa  37712  fdc  37724  sstotbnd2  37753  sstotbnd3  37755  igenidl  38042  prnc  38046  toycom  38951  lkrlss  39073  atlatmstc  39297  atlatle  39298  glbconN  39355  glbconNOLD  39356  linepsubN  39731  pmapssat  39738  pmaple  39740  pmapsub  39747  paddssat  39793  diass  41021  diaglbN  41034  diaintclN  41037  diassdvaN  41039  docaclN  41103  dibglbN  41145  dibintclN  41146  diclspsn  41173  dihglblem2N  41273  dih1dimatlem  41308  dihglb2  41321  dochval2  41331  dochcl  41332  dochvalr  41336  doch2val2  41343  dochss  41344  dochocss  41345  lclkr  41512  lclkrs  41518  lcdvbase  41572  lcdvbasess  41573  mapdunirnN  41629  aks4d1p4  42052  aks4d1p5  42053  aks4d1p7  42056  aks4d1p8  42060  sticksstones1  42119  aks6d1c6lem2  42144  grpods  42167  unitscyglem1  42168  unitscyglem2  42169  unitscyglem4  42171  mhpind  42567  mhphf  42570  prjcrv0  42606  infdesc  42616  mzpindd  42719  fiphp3d  42792  rencldnfilem  42793  irrapx1  42801  pellexlem3  42804  pellfundre  42854  pellfundge  42855  pellfundlb  42857  pellfundglb  42858  jm2.22  42968  jm2.23  42969  rpnnen3  43005  pwssplit4  43062  pwfi2f1o  43069  hbtlem6  43102  dgraalem  43118  dgraaub  43121  itgocn  43137  onintunirab  43200  nadd2rabord  43358  nadd1rabord  43362  rfovcnvf1od  43977  fsovfd  43985  fsovcnvlem  43986  binomcxplemdvbinom  44326  binomcxplemcvg  44327  binomcxplemnotnn0  44329  uzwo4  45031  disjf1o  45169  icof  45197  allbutfiinf  45400  supminfxr  45444  supminfxr2  45449  fsumsupp0  45560  sumnnodd  45612  fnlimabslt  45661  liminfvalxr  45765  ioodvbdlimc1lem1  45913  dvnprodlem1  45928  dvnprodlem2  45929  stoweidlem14  45996  stoweidlem34  46016  stoweidlem44  46026  stoweidlem50  46032  stoweidlem51  46033  stoweidlem52  46034  stoweidlem57  46039  stoweidlem59  46041  fourierdlem19  46108  fourierdlem20  46109  fourierdlem25  46114  fourierdlem31  46120  fourierdlem37  46126  fourierdlem42  46131  fourierdlem51  46139  fourierdlem54  46142  fourierdlem64  46152  fourierdlem79  46167  elaa2lem  46215  etransclem16  46232  etransclem24  46240  etransclem31  46247  etransclem33  46249  etransclem34  46250  etransclem48  46264  salgencl  46314  salexct  46316  salgenuni  46319  subsaliuncllem  46339  meadjiunlem  46447  caragenss  46486  caratheodory  46510  ovnlecvr  46540  ovnlerp  46544  ovn0lem  46547  ovnsubaddlem1  46552  hoidmv1lelem1  46573  hoidmv1lelem3  46575  hoidmvlelem1  46577  hoidmvlelem2  46578  hoidmvlelem3  46579  hoidmvlelem4  46580  ovnhoilem1  46583  ovnhoilem2  46584  ovnlecvr2  46592  ovncvr2  46593  opnvonmbllem2  46615  ovolval4lem1  46631  pimconstlt1  46684  pimiooltgt  46692  pimgtmnf2  46696  pimdecfgtioc  46697  pimincfltioc  46698  pimdecfgtioo  46699  pimincfltioo  46700  sssmf  46720  incsmflem  46723  smfaddlem1  46745  smfaddlem2  46746  decsmflem  46748  smflimlem1  46753  smflimlem2  46754  smflimlem3  46755  smfrec  46771  smfmullem4  46776  smfdiv  46779  smfsuplem1  46793  smfsuplem3  46795  smfinflem  46799  smflimsuplem1  46802  smflimsuplem7  46808  smfliminflem  46812  sprsymrelfolem1  47477  prmdvdsfmtnof1lem1  47569  prmdvdsfmtnof  47571  perfectALTVlem2  47707  isubgredg  47851  isubgruhgr  47853  isubgrgrim  47914  uhgrimisgrgric  47916  uspgrlimlem1  47973  uspgrlimlem4  47976  uspgrlim  47977  grlimgrtrilem2  47987  oddibas  48158  2zlidl  48225  2zrngbas  48227  2zrng0  48229  isclatd  48968  topclat  48983