MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssrab2 Structured version   Visualization version   GIF version

Theorem ssrab2 3834
Description: Subclass relation for a restricted class. (Contributed by NM, 19-Mar-1997.)
Assertion
Ref Expression
ssrab2 {𝑥𝐴𝜑} ⊆ 𝐴
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem ssrab2
StepHypRef Expression
1 df-rab 3069 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
2 ssab2 3833 . 2 {𝑥 ∣ (𝑥𝐴𝜑)} ⊆ 𝐴
31, 2eqsstri 3782 1 {𝑥𝐴𝜑} ⊆ 𝐴
Colors of variables: wff setvar class
Syntax hints:  wa 382  wcel 2144  {cab 2756  {crab 3064  wss 3721
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-rab 3069  df-in 3728  df-ss 3735
This theorem is referenced by:  ssrab3  3835  ssrabeq  3837  iinrab2  4715  riinrab  4728  rabexg  4942  pwnss  4958  frminex  5229  wereu2  5246  dmmptss  5775  wfisg  5858  ssimaex  6405  f1oresrab  6537  weniso  6746  canth  6750  riotacl  6767  riotassuni  6790  onminesb  7144  onminsb  7145  onintrab  7147  onnminsb  7150  onminex  7153  tfis  7200  omsson  7215  suppssdm  7458  fnsuppres  7473  oawordeulem  7787  oeeulem  7834  nnawordex  7870  pmvalg  8019  fineqvlem  8329  ordtypelem2  8579  ordtypelem3  8580  ordtypelem4  8581  ordtypelem6  8583  hartogs  8604  wemapso2lem  8612  card2on  8614  wdom2d  8640  oemapvali  8744  wemapwe  8757  tz9.12lem1  8813  tz9.12lem3  8815  rankf  8820  cplem1  8915  cardf2  8968  cardid2  8978  cardmin2  9023  acni3  9069  dfac2a  9151  cofsmo  9292  coftr  9296  fin2i2  9341  isfin2-2  9342  enfin2i  9344  fin23lem28  9363  fin23lem30  9365  isf32lem5  9380  isf32lem6  9381  isf32lem7  9382  isf32lem8  9383  fin1a2lem11  9433  fin1a2lem12  9434  hsmexlem4  9452  hsmexlem5  9453  hsmexlem6  9454  axdc3lem4  9476  ac6num  9502  ac6  9503  zorn2lem1  9519  zorn2lem3  9521  zorn2lem4  9522  zorn2lem5  9523  ondomon  9586  alephval2  9595  pwfseqlem1  9681  pwfseqlem3  9683  wunccl  9767  tskmcl  9864  0nnq  9947  elpqn  9948  fiminre  11173  infm3  11183  uzf  11890  nnwos  11957  supminf  11977  zsupss  11979  rpnnen1lem2  12016  rpnnen1lem1  12017  rpnnen1lem3  12018  rpnnen1lem5  12020  rpnnen1lem1OLD  12023  rpnnen1lem3OLD  12024  rpnnen1lem5OLD  12026  rpre  12041  ixxf  12389  fzf  12536  flval3  12823  rabssnn0fi  12992  expge0  13102  expge1  13103  hashbclem  13437  sqrlem3  14192  sqrlem5  14194  rlimrege0  14517  incexc2  14776  dvdsflip  15247  divalglem2  15325  divalglem5  15327  divalglem8  15330  bitsf  15356  bitsfzolem  15363  sadadd2lem  15388  sadadd3  15390  sadcl  15391  smupf  15407  smuval2  15411  smupvallem  15412  smucl  15413  smueqlem  15419  gcdcllem3  15430  bezoutlem2  15464  bezoutlem3  15465  lcmcllem  15516  lcmn0cl  15517  lcmledvds  15519  lcmfval  15541  lcmfcllem  15545  lcmfn0cl  15546  lcmfledvds  15552  maxprmfct  15627  phicl2  15679  phibnd  15682  hashdvds  15686  phiprmpw  15687  phimullem  15690  eulerthlem2  15693  eulerth  15694  phisum  15701  odzcllem  15703  odzdvds  15706  pclem  15749  infpn2  15823  prmreclem1  15826  prmreclem2  15827  prmreclem3  15828  prmreclem4  15829  prmreclem5  15830  4sqlem13  15867  4sqlem14  15868  4sqlem17  15871  4sqlem18  15872  vdwnnlem3  15907  hashbccl  15913  ramcl2lem  15919  ramtcl  15920  ramtcl2  15921  ramtub  15922  prmgaplem3  15963  prmgaplem4  15964  prdsds  16331  imasdsval2  16383  mrcflem  16473  isacs1i  16524  wunnat  16822  dmcoass  16922  lublecl  17196  lubid  17197  gsumval1  17484  issubmd  17556  mhmeql  17571  nmzsubg  17842  nmznsg  17845  conjnmz  17901  conjnmzb  17902  gastacl  17948  cntzval  17960  cntzssv  17967  symgsssg  18093  symgfisg  18094  pmtrdifellem4  18105  odlem1  18160  odlem2  18164  odngen  18198  gexlem1  18200  gexlem2  18203  sylow1lem2  18220  sylow1lem3  18221  sylow1lem4  18222  sylow1lem5  18223  sylow2alem2  18239  sylow2a  18240  sylow2blem3  18243  sylow3lem2  18249  oddvdssubg  18464  cyggex2  18504  ablfacrplem  18671  ablfacrp2  18673  ablfac1eu  18679  pgpfaclem1  18687  ablfaclem2  18692  ablfaclem3  18693  lssacs  19179  lspf  19186  lspsolvlem  19355  lbsextlem2  19373  lbsextlem3  19374  lbsextlem4  19375  rrgeq0  19504  rrgss  19506  asplss  19543  aspsubrg  19545  psrbagconf1o  19588  psrass1lem  19591  psrdi  19620  psrdir  19621  psrass23l  19622  psrass23  19624  resspsrmul  19631  mplbas  19643  mplbasss  19646  mplsubglem  19648  mplsubrglem  19653  mplmonmul  19678  psropprmul  19822  coe1mul2lem2  19852  cygznlem2a  20130  psgnghm  20140  ocvfval  20226  ocvval  20227  dsmmbase  20295  dsmmval2  20296  dsmmsubg  20303  frlmsslsp  20351  scmatlss  20548  smadiadet  20694  pmatcoe1fsupp  20725  cpmatsubgpmat  20744  fctop  21028  cctop  21030  ppttop  21031  epttop  21033  clscld  21071  mretopd  21116  neips  21137  neiptopnei  21156  ordtbaslem  21212  ordtuni  21214  ordtcld1  21221  ordtcld2  21222  cnpfval  21258  iscnp2  21263  cmpcov2  21413  cmpsublem  21422  tgcmp  21424  hauscmplem  21429  conncompcld  21457  1stcfb  21468  2ndc1stc  21474  2ndcdisj  21479  finlocfin  21543  kgentopon  21561  xkotf  21608  txkgen  21675  xkococnlem  21682  imastopn  21743  kqffn  21748  opnfbas  21865  flimfnfcls  22051  alexsubALT  22074  ptcmplem1  22075  ptcmplem2  22076  ptcmplem3  22077  symgtgp  22124  tgpconncompeqg  22134  tgpconncomp  22135  ghmcnp  22137  tsmsfbas  22150  eltsms  22155  utoptop  22257  utopbas  22258  imasdsf1olem  22397  blfvalps  22407  blfps  22430  blf  22431  blcld  22529  nmoffn  22734  nmofval  22737  nmogelb  22739  nmolb  22740  nmof  22742  icccmplem1  22844  icccmplem2  22845  icccmplem3  22846  ishtpy  22990  clsocv  23267  rrxnm  23397  rrxf  23402  minveclem3b  23417  minveclem4  23421  ivthlem1  23438  ivthlem2  23439  ivthlem3  23440  ovolcl  23465  ovollb  23466  ovolgelb  23467  ovolge0  23468  ovolsslem  23471  ovolshftlem1  23496  ovolshft  23498  ovolscalem1  23500  ovolscalem2  23501  ovolsca  23502  ovolicc2lem3  23506  ovolicc2lem4  23507  ovolicc2lem5  23508  ovolicc2  23509  shftmbl  23525  iundisj  23535  dyadmax  23585  dyadmbllem  23586  dyadmbl  23587  opnmbllem  23588  iblmbf  23753  mdegmullem  24057  uc1pval  24118  mon1pval  24120  elqaalem1  24293  elqaalem3  24295  aannenlem2  24303  aalioulem2  24307  radcnvcl  24390  radcnvlt1  24391  radcnvle  24393  abelthlem4  24407  abelthlem6  24409  abelthlem9  24413  abelth  24414  atancn  24883  lgamucov  24984  lgamucov2  24985  ftalem3  25021  ftalem4  25022  ftalem5  25023  efnnfsumcl  25049  isppw  25060  sgmval2  25089  efchtdvds  25105  sqff1o  25128  fsumdvdsdiaglem  25129  fsumdvdsdiag  25130  fsumdvdscom  25131  musum  25137  muinv  25139  dvdsmulf1o  25140  fsumdvdsmul  25141  sgmmul  25146  ppiub  25149  vmasum  25161  logfac2  25162  perfectlem2  25175  lgsfcl2  25248  lgsfcl  25250  lgscl  25256  lgsquadlem1  25325  lgsquadlem2  25326  rpvmasumlem  25396  rpvmasum2  25421  dchrisum0re  25422  dchrisum0lema  25423  dchrisum0lem1b  25424  dchrisum0lem1  25425  dchrisum0lem2a  25426  dchrisum0lem2  25427  dchrisum0lem3  25428  dchrisum0  25429  mudivsum  25439  mulogsum  25441  mulog2sumlem2  25444  vmalogdivsum2  25447  logsqvma  25451  logsqvma2  25452  selberglem3  25456  selberg  25457  selberg34r  25480  pntsval2  25485  pntrlog2bndlem1  25486  pntlem3  25518  tglnunirn  25663  tglnssp  25667  axcontlem2  26065  axcontlem7  26070  axcontlem8  26071  axcontlem10  26073  incistruhgr  26194  upgrss  26203  upgrn0  26204  upgruhgr  26217  usgrss  26290  uspgrushgr  26291  ushgredgedg  26342  ushgredgedgloop  26344  ushgredgedgloopOLD  26345  upgrreslem  26418  umgrreslem  26419  vtxdun  26611  vtxdginducedm1lem2  26670  vtxdginducedm1  26673  finsumvtxdg2ssteplem1  26675  hashwwlksnext  27056  clwwlksswrd  27134  frcond3  27448  numclwlk1lem2  27556  ocsh  28476  spancl  28529  shsval2i  28580  ococin  28601  chsupid  28605  speccl  29092  atssch  29536  hatomistici  29555  chpssati  29556  iundisjf  29734  aciunf1  29797  fcobijfs  29835  fpwrelmap  29842  iundisjfi  29889  locfinreflem  30241  esumrnmpt2  30464  esumpinfval  30469  sigagensiga  30538  ldgenpisyslem1  30560  ldgenpisys  30563  measvuni  30611  imambfm  30658  dya2iocuni  30679  omscl  30691  oms0  30693  omsmon  30694  omssubadd  30696  carsgcl  30700  oddpwdc  30750  eulerpartlem1  30763  eulerpartlemt  30767  eulerpartgbij  30768  eulerpartlemmf  30771  eulerpartlemgh  30774  eulerpartlemgs2  30776  ballotlem2  30884  ballotlemfc0  30888  ballotlemfcc  30889  ballotlemfmpn  30890  ballotlemiex  30897  ballotlemsup  30900  ballotlem7  30931  ballotth  30933  reprpmtf1o  31038  breprexplema  31042  hgt750lema  31069  bnj110  31260  bnj1204  31412  bnj1311  31424  subfacp1lem3  31496  subfacp1lem5  31498  subfacp1lem6  31499  erdszelem2  31506  connpconn  31549  cvmliftmolem2  31596  cvmliftlem15  31612  cvmlift2lem12  31628  snmlff  31643  tfisg  32046  frpomin  32069  frpoinsg  32072  frinsg  32076  wlimss  32105  sltval2  32140  conway  32241  scutun12  32248  scutbdaybnd  32252  scutbdaylt  32253  rankeq1o  32609  finminlem  32643  fnessref  32683  neibastop1  32685  neibastop2lem  32686  bj-rabtr  33252  bj-rabtrALTALT  33254  bj-rabtrAUTO  33255  bj-cmnssmnd  33466  bj-vecssmod  33473  bj-rrvecssvec  33480  icoreresf  33530  phpreu  33719  fin2so  33722  poimirlem26  33761  poimirlem31  33766  poimirlem32  33767  opnmbllem0  33771  mblfinlem1  33772  mblfinlem2  33773  ismblfin  33776  mbfposadd  33782  cnambfre  33783  cover2  33833  indexa  33853  fdc  33866  sstotbnd2  33898  sstotbnd3  33900  igenidl  34187  prnc  34191  toycom  34775  lkrlss  34897  atlatmstc  35121  atlatle  35122  glbconN  35178  linepsubN  35553  pmapssat  35560  pmaple  35562  pmapsub  35569  paddssat  35615  diass  36845  diaglbN  36858  diaintclN  36861  diassdvaN  36863  docaclN  36927  dibglbN  36969  dibintclN  36970  diclspsn  36997  dihglblem2N  37097  dih1dimatlem  37132  dihglb2  37145  dochval2  37155  dochcl  37156  dochvalr  37160  doch2val2  37167  dochss  37168  dochocss  37169  lclkr  37336  lclkrs  37342  lcdvbase  37396  lcdvbasess  37397  mapdunirnN  37453  mzpindd  37828  fiphp3d  37902  rencldnfilem  37903  irrapx1  37911  pellexlem3  37914  pellfundre  37964  pellfundge  37965  pellfundlb  37967  pellfundglb  37968  jm2.22  38081  jm2.23  38082  rpnnen3  38118  fglmod  38162  pwssplit4  38178  pwfi2f1o  38185  hbtlem6  38218  dgraalem  38234  dgraaub  38237  itgocn  38253  rgspncl  38258  rfovcnvf1od  38817  fsovfd  38825  fsovcnvlem  38826  binomcxplemdvbinom  39071  binomcxplemcvg  39072  binomcxplemnotnn0  39074  uzwo4  39736  disjf1o  39892  icof  39923  allbutfiinf  40157  supminfxr  40204  supminfxr2  40209  fsumsupp0  40322  limcperiod  40372  sumnnodd  40374  fnlimabslt  40423  liminfvalxr  40527  cncfshift  40599  cncfperiod  40604  ioodvbdlimc1lem1  40658  dvnprodlem1  40673  dvnprodlem2  40674  stoweidlem14  40742  stoweidlem34  40762  stoweidlem44  40772  stoweidlem50  40778  stoweidlem51  40779  stoweidlem52  40780  stoweidlem57  40785  stoweidlem59  40787  fourierdlem19  40854  fourierdlem20  40855  fourierdlem25  40860  fourierdlem31  40866  fourierdlem37  40872  fourierdlem42  40877  fourierdlem51  40885  fourierdlem54  40888  fourierdlem64  40898  fourierdlem79  40913  elaa2lem  40961  etransclem16  40978  etransclem24  40986  etransclem31  40993  etransclem33  40995  etransclem34  40996  etransclem48  41010  rrxbasefi  41014  salgencl  41061  salexct  41063  salgenuni  41066  subsaliuncllem  41086  meadjiunlem  41193  caragenss  41232  caratheodory  41256  ovnlecvr  41286  ovnsslelem  41288  ovnlerp  41290  ovn0lem  41293  ovnsubaddlem1  41298  hoidmv1lelem1  41319  hoidmv1lelem3  41321  hoidmvlelem1  41323  hoidmvlelem2  41324  hoidmvlelem3  41325  hoidmvlelem4  41326  ovnhoilem1  41329  ovnhoilem2  41330  ovnlecvr2  41338  ovncvr2  41339  opnvonmbllem2  41361  ovolval4lem1  41377  ovolval5lem3  41382  pimconstlt1  41429  pimltpnf  41430  pimiooltgt  41435  pimgtmnf2  41438  pimdecfgtioc  41439  pimincfltioc  41440  pimdecfgtioo  41441  pimincfltioo  41442  sssmf  41461  incsmflem  41464  smfaddlem1  41485  smfaddlem2  41486  decsmflem  41488  smflimlem1  41493  smflimlem2  41494  smflimlem3  41495  smfrec  41510  smfmullem4  41515  smfdiv  41518  smfsuplem1  41531  smfsuplem3  41533  smfinflem  41537  smflimsuplem1  41540  smflimsuplem7  41546  smfliminflem  41550  prmdvdsfmtnof1lem1  42014  prmdvdsfmtnof  42016  perfectALTVlem2  42149  sprsymrelfolem1  42260  rabsubmgmd  42309  mgmhmeql  42321  oddibas  42331  2zlidl  42452  2zrngbas  42454  2zrng0  42456
  Copyright terms: Public domain W3C validator