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

Theorem ssrab2 3432
Description: Subclass relation for a restricted class. (Contributed by NM, 19-Mar-1997.)
Assertion
Ref Expression
ssrab2  |-  { x  e.  A  |  ph }  C_  A
Distinct variable group:    x, A
Allowed substitution hint:    ph( x)

Proof of Theorem ssrab2
StepHypRef Expression
1 df-rab 2719 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
2 ssab2 3431 . 2  |-  { x  |  ( x  e.  A  /\  ph ) }  C_  A
31, 2eqsstri 3381 1  |-  { x  e.  A  |  ph }  C_  A
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    e. wcel 1756   {cab 2424   {crab 2714    C_ wss 3323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2719  df-in 3330  df-ss 3337
This theorem is referenced by:  ssrabeq  3433  iinrab2  4228  riinrab  4241  rabexg  4437  pwnss  4452  frminex  4695  wereu2  4712  dmmptss  5329  ssimaex  5751  f1oresrab  5870  fnsuppresOLD  5933  weniso  6040  canth  6044  riotacl  6062  riotassuniOLD  6084  onminesb  6404  onminsb  6405  onintrab  6407  onnminsb  6410  onminex  6413  tfis  6460  omsson  6475  suppssdm  6698  fnsuppres  6711  oawordeulem  6985  oeeulem  7032  nnawordex  7068  pmvalg  7217  fineqvlem  7519  ordtypelem2  7725  ordtypelem3  7726  ordtypelem4  7727  ordtypelem6  7729  hartogs  7750  wemapso2OLD  7758  wemapso2lem  7759  card2on  7761  wdom2d  7787  oemapvali  7884  wemapwe  7920  wemapweOLD  7921  tz9.12lem1  7986  tz9.12lem3  7988  rankf  7993  cplem1  8088  cardf2  8105  cardid2  8115  cardmin2  8160  acni3  8209  dfac2a  8291  cofsmo  8430  coftr  8434  fin2i2  8479  isfin2-2  8480  enfin2i  8482  fin23lem28  8501  fin23lem30  8503  isf32lem5  8518  isf32lem6  8519  isf32lem7  8520  isf32lem8  8521  fin1a2lem11  8571  fin1a2lem12  8572  hsmexlem4  8590  hsmexlem5  8591  hsmexlem6  8592  axdc3lem4  8614  ac6num  8640  ac6  8641  zorn2lem1  8657  zorn2lem3  8659  zorn2lem4  8660  zorn2lem5  8661  ondomon  8719  alephval2  8728  pwfseqlem1  8817  pwfseqlem3  8819  wunccl  8903  tskmcl  9000  0nnq  9085  elpqn  9086  infm3  10281  infmrcl  10301  uzf  10856  nnwos  10914  supminf  10934  zsupss  10936  rpnnen1lem1  10971  rpnnen1lem2  10972  rpnnen1lem3  10973  rpnnen1lem5  10975  rpre  10989  ixxf  11302  fzf  11433  flval3  11655  expge0  11892  expge1  11893  hashbclem  12197  sqrlem3  12726  sqrlem5  12728  rlimrege0  13049  incexc2  13293  divalglem2  13591  divalglem5  13593  divalglem8  13596  bitsf  13615  bitsfzolem  13622  sadadd2lem  13647  sadadd3  13649  sadcl  13650  smupf  13666  smuval2  13670  smupvallem  13671  smucl  13672  smueqlem  13678  gcdcllem3  13689  bezoutlem2  13715  bezoutlem3  13716  maxprmfct  13791  phicl2  13835  phibnd  13838  hashdvds  13842  phiprmpw  13843  phimullem  13846  eulerthlem2  13849  eulerth  13850  odzcllem  13856  odzdvds  13859  pclem  13897  infpn2  13966  prmreclem1  13969  prmreclem2  13970  prmreclem3  13971  prmreclem4  13972  prmreclem5  13973  4sqlem13  14010  4sqlem14  14011  4sqlem17  14014  4sqlem18  14015  vdwnnlem3  14050  hashbccl  14056  ramcl2lem  14062  ramtcl  14063  ramtcl2  14064  ramtub  14065  prdsds  14394  imasdsval2  14446  mrcflem  14536  isacs1i  14587  wunnat  14858  dmcoass  14926  lublecl  15151  lubid  15152  issubmd  15468  mhmeql  15483  gsumval1  15500  nmzsubg  15713  nmznsg  15716  conjnmz  15771  conjnmzb  15772  gastacl  15818  cntzval  15830  cntzssv  15837  symgsssg  15964  symgfisg  15965  pmtrdifellem4  15976  odlem1  16029  odlem2  16033  odngen  16067  gexlem1  16069  gexlem2  16072  sylow1lem2  16089  sylow1lem3  16090  sylow1lem4  16091  sylow1lem5  16092  sylow2alem2  16108  sylow2a  16109  sylow2blem3  16112  sylow3lem2  16118  oddvdssubg  16328  cyggex2  16364  ablfacrplem  16554  ablfacrp2  16556  ablfac1eu  16562  pgpfaclem1  16570  ablfaclem2  16575  ablfaclem3  16576  lssacs  17025  lspf  17032  lspsolvlem  17200  lbsextlem2  17217  lbsextlem3  17218  lbsextlem4  17219  rrgeq0  17338  rrgss  17341  asplss  17377  aspsubrg  17379  psrbagconf1o  17421  psrass1lem  17424  psrdi  17456  psrdir  17457  psrass23  17459  resspsrmul  17466  mplbas  17480  mplbasOLD  17482  mplbasss  17485  mplsubglem  17487  mplsubglemOLD  17489  mplsubrglem  17494  mplsubrglemOLD  17495  mplmonmul  17520  psropprmul  17668  coe1mul2lem2  17697  cygznlem2a  17975  psgnghm  17985  ocvfval  18066  ocvval  18067  dsmmbase  18135  dsmmval2  18136  dsmmsubg  18143  frlmsslsp  18198  frlmsslspOLD  18199  smadiadet  18451  fctop  18583  cctop  18585  ppttop  18586  epttop  18588  clscld  18626  mretopd  18671  neips  18692  neiptopnei  18711  ordtbaslem  18767  ordtuni  18769  ordtcld1  18776  ordtcld2  18777  cnpfval  18813  iscnp2  18818  cmpcov2  18968  cmpsublem  18977  tgcmp  18979  hauscmplem  18984  concompcld  19013  1stcfb  19024  2ndc1stc  19030  2ndcdisj  19035  kgentopon  19086  xkotf  19133  txkgen  19200  xkococnlem  19207  imastopn  19268  kqffn  19273  opnfbas  19390  flimfnfcls  19576  alexsubALT  19598  ptcmplem1  19599  ptcmplem2  19600  ptcmplem3  19601  symgtgp  19647  tgpconcompeqg  19657  tgpconcomp  19658  ghmcnp  19660  tsmsfbas  19673  eltsms  19678  utoptop  19784  utopbas  19785  imasdsf1olem  19923  blfvalps  19933  blfps  19956  blf  19957  blcld  20055  nmoffn  20265  nmofval  20268  nmogelb  20270  nmolb  20271  nmof  20273  icccmplem1  20374  icccmplem2  20375  icccmplem3  20376  ishtpy  20519  clsocv  20737  rrxnm  20870  rrxf  20875  minveclem3b  20890  minveclem4  20894  ivthlem1  20910  ivthlem2  20911  ivthlem3  20912  ovolcl  20936  ovollb  20937  ovolgelb  20938  ovolge0  20939  ovolsslem  20942  ovolshftlem1  20967  ovolshft  20969  ovolscalem1  20971  ovolscalem2  20972  ovolsca  20973  ovolicc2lem3  20977  ovolicc2lem4  20978  ovolicc2lem5  20979  ovolicc2  20980  shftmbl  20995  iundisj  21004  dyadmax  21053  dyadmbllem  21054  dyadmbl  21055  opnmbllem  21056  iblmbf  21220  mdegmullem  21524  uc1pval  21586  mon1pval  21588  elqaalem1  21760  elqaalem3  21762  aannenlem2  21770  aalioulem2  21774  radcnvcl  21857  radcnvlt1  21858  radcnvle  21860  abelthlem4  21874  abelthlem6  21876  abelthlem9  21880  abelth  21881  atancn  22306  ftalem3  22387  ftalem4  22388  ftalem5  22389  efnnfsumcl  22415  isppw  22427  sgmval2  22456  efchtdvds  22472  sqff1o  22495  dvdsflip  22497  fsumdvdsdiaglem  22498  fsumdvdsdiag  22499  fsumdvdscom  22500  musum  22506  muinv  22508  dvdsmulf1o  22509  fsumdvdsmul  22510  sgmmul  22515  ppiub  22518  vmasum  22530  logfac2  22531  perfectlem2  22544  lgsfcl2  22616  lgsfcl  22618  lgscl  22624  lgsquadlem1  22668  lgsquadlem2  22669  rpvmasumlem  22711  rpvmasum2  22736  dchrisum0re  22737  dchrisum0lema  22738  dchrisum0lem1b  22739  dchrisum0lem1  22740  dchrisum0lem2a  22741  dchrisum0lem2  22742  dchrisum0lem3  22743  dchrisum0  22744  mudivsum  22754  mulogsum  22756  mulog2sumlem2  22759  vmalogdivsum2  22762  logsqvma  22766  logsqvma2  22767  selberglem3  22771  selberg  22772  selberg34r  22795  pntsval2  22800  pntrlog2bndlem1  22801  pntlem3  22833  tglnunirn  22957  tglnssp  22960  axcontlem2  23162  axcontlem7  23167  axcontlem8  23168  axcontlem10  23170  umgrass  23204  umgran0  23205  umisuhgra  23212  usgrass  23234  usgrares1  23274  usgrafilem1  23275  nbgrassvt  23295  nbgraf1olem1  23301  cusgrares  23331  vdgrun  23522  vdgrfiun  23523  konigsberg  23559  ocsh  24637  spancl  24690  shsval2i  24741  ococin  24762  chsupid  24766  speccl  25254  atssch  25698  hatomistici  25717  chpssati  25718  iundisjf  25882  fcobijfs  25977  fpwrelmap  25984  iundisjfi  26031  esumpinfval  26474  sigagensiga  26536  measvuni  26580  imambfm  26629  dya2iocuni  26650  oms0  26662  omsmon  26663  oddpwdc  26689  eulerpartlem1  26702  eulerpartlemt  26706  eulerpartgbij  26707  eulerpartlemmf  26710  eulerpartlemgvv  26711  eulerpartlemgh  26713  eulerpartlemgs2  26715  ballotlemoex  26820  ballotlem2  26823  ballotlemfc0  26827  ballotlemfcc  26828  ballotlemfmpn  26829  ballotlemiex  26836  ballotlemsup  26839  ballotlem7  26870  ballotth  26872  lgamucov  26976  lgamucov2  26977  subfacp1lem3  27022  subfacp1lem5  27024  subfacp1lem6  27025  erdszelem2  27032  conpcon  27076  cvmliftmolem2  27123  cvmliftlem15  27139  cvmlift2lem12  27155  snmlff  27170  tfisg  27616  wfisg  27621  frinsg  27657  wlimss  27717  sltval2  27748  nodenselem4  27776  nobndlem5  27788  nofulllem5  27798  rankeq1o  28160  fin2so  28369  opnmbllem0  28380  mblfinlem1  28381  mblfinlem2  28382  ismblfin  28385  mbfposadd  28392  cnambfre  28393  finminlem  28466  fnessref  28518  finlocfin  28524  neibastop1  28533  neibastop2lem  28534  cover2  28560  indexa  28580  fdc  28594  sstotbnd2  28626  sstotbnd3  28628  igenidl  28816  prnc  28820  mzpindd  29035  fiphp3d  29111  rencldnfilem  29112  irrapx1  29122  pellexlem3  29125  pellfundre  29175  pellfundge  29176  pellfundlb  29178  pellfundglb  29179  jm2.22  29297  jm2.23  29298  rpnnen3  29334  fglmod  29379  pwssplit4  29395  pwfi2f1o  29404  hbtlem6  29438  dgraalem  29455  dgraaub  29458  itgocn  29474  rgspncl  29479  phisum  29520  stoweidlem14  29762  stoweidlem34  29782  stoweidlem44  29792  stoweidlem50  29798  stoweidlem51  29799  stoweidlem52  29800  stoweidlem57  29805  stoweidlem59  29807  clwwlksswrd  30393  hashwwlkext  30518  frisusgranb  30542  frgrawopreg1  30596  frgrawopreg2  30597  rabssnn0fi  30698  fsuppmapnn0fz  30746  psrass23l  30763  dmatsgrp  30801  scmatsgrp  30808  pmatcollpw2lem  30820  bnj21  31593  bnj110  31738  bnj1204  31890  bnj1311  31902  bj-rabtr  32281  bj-rabtrAUTO  32283  bj-vecmod  32419  bj-rrvecvec  32429  toycom  32458  lkrlss  32580  atlatmstc  32804  atlatle  32805  glbconN  32861  linepsubN  33236  pmapssat  33243  pmaple  33245  pmapsub  33252  paddssat  33298  diass  34527  diaglbN  34540  diaintclN  34543  diassdvaN  34545  docaclN  34609  dibglbN  34651  dibintclN  34652  diclspsn  34679  dihglblem2N  34779  dih1dimatlem  34814  dihglb2  34827  dochval2  34837  dochcl  34838  dochvalr  34842  doch2val2  34849  dochss  34850  dochocss  34851  lclkr  35018  lclkrs  35024  lcdvbase  35078  lcdvbasess  35079  mapdunirnN  35135
  Copyright terms: Public domain W3C validator