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

Theorem ssrab2 3489
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 2723 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
2 ssab2 3488 . 2  |-  { x  |  ( x  e.  A  /\  ph ) }  C_  A
31, 2eqsstri 3437 1  |-  { x  e.  A  |  ph }  C_  A
Colors of variables: wff setvar class
Syntax hints:    /\ wa 370    e. wcel 1872   {cab 2414   {crab 2718    C_ wss 3379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-rab 2723  df-in 3386  df-ss 3393
This theorem is referenced by:  ssrabeq  3490  iinrab2  4305  riinrab  4318  rabexg  4517  pwnss  4532  frminex  4776  wereu2  4793  dmmptss  5293  wfisg  5377  ssimaex  5890  f1oresrab  6014  weniso  6204  canth  6208  riotacl  6225  riotassuni  6247  onminesb  6583  onminsb  6584  onintrab  6586  onnminsb  6589  onminex  6592  tfis  6639  omsson  6654  suppssdm  6882  fnsuppres  6897  oawordeulem  7210  oeeulem  7257  nnawordex  7293  pmvalg  7438  fineqvlem  7739  ordtypelem2  7987  ordtypelem3  7988  ordtypelem4  7989  ordtypelem6  7991  hartogs  8012  wemapso2lem  8020  card2on  8022  wdom2d  8048  oemapvali  8141  wemapwe  8154  tz9.12lem1  8210  tz9.12lem3  8212  rankf  8217  cplem1  8312  cardf2  8329  cardid2  8339  cardmin2  8384  acni3  8429  dfac2a  8511  cofsmo  8650  coftr  8654  fin2i2  8699  isfin2-2  8700  enfin2i  8702  fin23lem28  8721  fin23lem30  8723  isf32lem5  8738  isf32lem6  8739  isf32lem7  8740  isf32lem8  8741  fin1a2lem11  8791  fin1a2lem12  8792  hsmexlem4  8810  hsmexlem5  8811  hsmexlem6  8812  axdc3lem4  8834  ac6num  8860  ac6  8861  zorn2lem1  8877  zorn2lem3  8879  zorn2lem4  8880  zorn2lem5  8881  ondomon  8939  alephval2  8948  pwfseqlem1  9034  pwfseqlem3  9036  wunccl  9120  tskmcl  9217  0nnq  9300  elpqn  9301  fiminre  10506  infm3  10519  infmrclOLD  10544  uzf  11113  nnwos  11177  supminf  11201  supminfOLD  11202  zsupss  11204  rpnnen1lem1  11241  rpnnen1lem2  11242  rpnnen1lem3  11243  rpnnen1lem5  11245  rpre  11259  ixxf  11596  fzf  11739  flval3  12000  rabssnn0fi  12148  expge0  12258  expge1  12259  hashbclem  12563  sqrlem3  13252  sqrlem5  13254  rlimrege0  13586  incexc2  13839  divalglem2  14316  divalglem2OLD  14317  divalglem5OLD  14319  divalglem5  14320  divalglem8  14323  bitsf  14343  bitsfzolem  14350  bitsfzolemOLD  14351  sadadd2lem  14376  sadadd3  14378  sadcl  14379  smupf  14395  smuval2  14399  smupvallem  14400  smucl  14401  smueqlem  14407  gcdcllem3  14418  bezoutlem2OLD  14447  bezoutlem3OLD  14448  bezoutlem2  14450  bezoutlem3  14451  lcmcllem  14504  lcmn0cl  14505  lcmledvds  14507  lcmscllemOLD  14525  lcmsnnOLD  14526  lcmsledvdsOLD  14528  lcmfval  14534  lcmfvalOLD  14538  lcmfcllem  14541  lcmfn0cl  14542  lcmfledvds  14548  maxprmfct  14595  phicl2  14659  phibnd  14662  hashdvds  14666  phiprmpw  14667  phimullem  14670  eulerthlem2  14673  eulerth  14674  odzcllem  14680  odzdvds  14683  odzcllemOLD  14686  odzdvdsOLD  14689  pclem  14731  infpn2  14800  prmreclem1  14803  prmreclem2  14804  prmreclem3  14805  prmreclem4  14806  prmreclem5  14807  4sqlem13OLD  14844  4sqlem14OLD  14845  4sqlem17OLD  14848  4sqlem18OLD  14849  4sqlem13  14850  4sqlem14  14851  4sqlem17  14854  4sqlem18  14855  vdwnnlem3  14890  hashbccl  14898  ramcl2lem  14905  ramcl2lemOLD  14906  ramtcl  14907  ramtclOLD  14908  ramtcl2  14909  ramtcl2OLD  14910  ramtub  14911  ramtubOLD  14912  prmordvdslcmsOLDOLD  14964  prmgaplem3  14966  prmgaplem4  14967  prdsds  15305  imasdsval2  15360  imasdsval2OLD  15372  mrcflem  15455  isacs1i  15506  wunnat  15804  dmcoass  15904  lublecl  16178  lubid  16179  gsumval1  16463  issubmd  16539  mhmeql  16554  nmzsubg  16801  nmznsg  16804  conjnmz  16859  conjnmzb  16860  gastacl  16906  cntzval  16918  cntzssv  16925  symgsssg  17051  symgfisg  17052  pmtrdifellem4  17063  odlem1  17124  odlem1OLD  17127  odlem2  17131  odlem2OLD  17147  odngen  17169  gexlem1  17171  gexlem1OLD  17173  gexlem2  17176  gexlem2OLD  17179  sylow1lem2  17194  sylow1lem3  17195  sylow1lem4  17196  sylow1lem5  17197  sylow2alem2  17213  sylow2a  17214  sylow2blem3  17217  sylow3lem2  17223  oddvdssubg  17436  cyggex2  17474  ablfacrplem  17641  ablfacrp2  17643  ablfac1eu  17649  pgpfaclem1  17657  ablfaclem2  17662  ablfaclem3  17663  lssacs  18133  lspf  18140  lspsolvlem  18308  lbsextlem2  18325  lbsextlem3  18326  lbsextlem4  18327  rrgeq0  18457  rrgss  18459  asplss  18496  aspsubrg  18498  psrbagconf1o  18541  psrass1lem  18544  psrdi  18573  psrdir  18574  psrass23l  18575  psrass23  18577  resspsrmul  18584  mplbas  18596  mplbasss  18599  mplsubglem  18601  mplsubrglem  18606  mplmonmul  18631  psropprmul  18774  coe1mul2lem2  18804  cygznlem2a  19080  psgnghm  19090  ocvfval  19171  ocvval  19172  dsmmbase  19240  dsmmval2  19241  dsmmsubg  19248  frlmsslsp  19296  scmatlss  19492  smadiadet  19637  pmatcoe1fsupp  19667  cpmatsubgpmat  19686  fctop  19961  cctop  19963  ppttop  19964  epttop  19966  clscld  20004  mretopd  20050  neips  20071  neiptopnei  20090  ordtbaslem  20146  ordtuni  20148  ordtcld1  20155  ordtcld2  20156  cnpfval  20192  iscnp2  20197  cmpcov2  20347  cmpsublem  20356  tgcmp  20358  hauscmplem  20363  concompcld  20391  1stcfb  20402  2ndc1stc  20408  2ndcdisj  20413  finlocfin  20477  kgentopon  20495  xkotf  20542  txkgen  20609  xkococnlem  20616  imastopn  20677  kqffn  20682  opnfbas  20799  flimfnfcls  20985  alexsubALT  21008  ptcmplem1  21009  ptcmplem2  21010  ptcmplem3  21011  symgtgp  21058  tgpconcompeqg  21068  tgpconcomp  21069  ghmcnp  21071  tsmsfbas  21084  eltsms  21089  utoptop  21191  utopbas  21192  imasdsf1olem  21330  blfvalps  21340  blfps  21363  blf  21364  blcld  21462  nmoffn  21658  nmofval  21661  nmogelb  21663  nmolb  21664  nmof  21666  nmoffnOLD  21679  nmofvalOLD  21680  nmogelbOLD  21682  nmolbOLD  21683  nmofOLD  21684  icccmplem1  21782  icccmplem2  21783  icccmplem3  21784  ishtpy  21945  clsocv  22163  rrxnm  22292  rrxf  22297  minveclem3b  22312  minveclem4  22316  minveclem3bOLD  22324  minveclem4OLD  22328  ivthlem1  22344  ivthlem2  22345  ivthlem3  22346  ovolcl  22373  ovollb  22374  ovolgelb  22375  ovolge0  22376  ovolsslem  22379  ovolshftlem1  22404  ovolshft  22406  ovolscalem1  22408  ovolscalem2  22409  ovolsca  22410  ovolicc2lem3  22414  ovolicc2lem4OLD  22415  ovolicc2lem4  22416  ovolicc2lem5  22417  ovolicc2  22418  shftmbl  22434  iundisj  22443  dyadmax  22498  dyadmbllem  22499  dyadmbl  22500  opnmbllem  22501  iblmbf  22667  mdegmullem  22969  uc1pval  23032  mon1pval  23034  elqaalem1  23214  elqaalem3  23216  elqaalem1OLD  23217  elqaalem3OLD  23219  aannenlem2  23227  aalioulem2  23231  radcnvcl  23314  radcnvlt1  23315  radcnvle  23317  abelthlem4  23331  abelthlem6  23333  abelthlem9  23337  abelth  23338  atancn  23804  lgamucov  23905  lgamucov2  23906  ftalem3  23941  ftalem4  23942  ftalem5  23943  ftalem4OLD  23944  ftalem5OLD  23945  efnnfsumcl  23971  isppw  23983  sgmval2  24012  efchtdvds  24028  sqff1o  24051  dvdsflip  24053  fsumdvdsdiaglem  24054  fsumdvdsdiag  24055  fsumdvdscom  24056  musum  24062  muinv  24064  dvdsmulf1o  24065  fsumdvdsmul  24066  sgmmul  24071  ppiub  24074  vmasum  24086  logfac2  24087  perfectlem2  24100  lgsfcl2  24172  lgsfcl  24174  lgscl  24180  lgsquadlem1  24224  lgsquadlem2  24225  rpvmasumlem  24267  rpvmasum2  24292  dchrisum0re  24293  dchrisum0lema  24294  dchrisum0lem1b  24295  dchrisum0lem1  24296  dchrisum0lem2a  24297  dchrisum0lem2  24298  dchrisum0lem3  24299  dchrisum0  24300  mudivsum  24310  mulogsum  24312  mulog2sumlem2  24315  vmalogdivsum2  24318  logsqvma  24322  logsqvma2  24323  selberglem3  24327  selberg  24328  selberg34r  24351  pntsval2  24356  pntrlog2bndlem1  24357  pntlem3  24389  tglnunirn  24535  tglnssp  24539  axcontlem2  24937  axcontlem7  24942  axcontlem8  24943  axcontlem10  24945  umgrass  24988  umgran0  24989  umisuhgra  24996  usgrass  25030  uslisushgra  25032  usgrares1  25080  usgrafilem1  25081  nbgrassvt  25103  nbgraf1olem1  25111  cusgrares  25142  hashwwlkext  25416  clwwlksswrd  25447  vdgrun  25571  vdgrfiun  25572  konigsberg  25657  frisusgranb  25667  frgrawopreg1  25720  frgrawopreg2  25721  ocsh  26878  spancl  26931  shsval2i  26982  ococin  27003  chsupid  27007  speccl  27494  atssch  27938  hatomistici  27957  chpssati  27958  iundisjf  28145  aciunf1  28211  fcobijfs  28261  fpwrelmap  28268  iundisjfi  28322  locfinreflem  28619  esumrnmpt2  28841  esumpinfval  28846  sigagensiga  28915  ldgenpisyslem1  28937  ldgenpisys  28940  measvuni  28988  imambfm  29036  dya2iocuni  29057  omscl  29071  omsclOLD  29075  oms0  29077  omsmon  29078  omssubadd  29080  oms0OLD  29081  omsmonOLD  29082  omssubaddOLD  29084  carsgcl  29088  oddpwdc  29139  eulerpartlem1  29152  eulerpartlemt  29156  eulerpartgbij  29157  eulerpartlemmf  29160  eulerpartlemgvv  29161  eulerpartlemgh  29163  eulerpartlemgs2  29165  ballotlem2  29273  ballotlemfc0  29277  ballotlemfcc  29278  ballotlemfmpn  29279  ballotlemiex  29286  ballotlemsup  29289  ballotlem7  29320  ballotth  29322  ballotlemiexOLD  29324  ballotlemsupOLD  29327  ballotlem7OLD  29358  ballotthOLD  29360  bnj21  29475  bnj110  29621  bnj1204  29773  bnj1311  29785  subfacp1lem3  29857  subfacp1lem5  29859  subfacp1lem6  29860  erdszelem2  29867  conpcon  29910  cvmliftmolem2  29957  cvmliftlem15  29973  cvmlift2lem12  29989  snmlff  30004  tfisg  30408  frinsg  30434  wlimss  30463  sltval2  30494  nodenselem4  30522  nobndlem5  30534  nofulllem5  30544  rankeq1o  30887  finminlem  30923  fnessref  30962  neibastop1  30964  neibastop2lem  30965  bj-rabtr  31444  bj-rabtrALTALT  31446  bj-rabtrAUTO  31447  bj-cmnssmnd  31598  bj-vecssmod  31605  bj-rrvecssvec  31612  icoreresf  31662  phpreu  31836  fin2so  31839  poimirlem26  31873  poimirlem31  31878  poimirlem32  31879  opnmbllem0  31883  mblfinlem1  31884  mblfinlem2  31885  ismblfin  31888  mbfposadd  31895  cnambfre  31896  cover2  31947  indexa  31967  fdc  31981  sstotbnd2  32013  sstotbnd3  32015  igenidl  32203  prnc  32207  toycom  32451  lkrlss  32573  atlatmstc  32797  atlatle  32798  glbconN  32854  linepsubN  33229  pmapssat  33236  pmaple  33238  pmapsub  33245  paddssat  33291  diass  34522  diaglbN  34535  diaintclN  34538  diassdvaN  34540  docaclN  34604  dibglbN  34646  dibintclN  34647  diclspsn  34674  dihglblem2N  34774  dih1dimatlem  34809  dihglb2  34822  dochval2  34832  dochcl  34833  dochvalr  34837  doch2val2  34844  dochss  34845  dochocss  34846  lclkr  35013  lclkrs  35019  lcdvbase  35073  lcdvbasess  35074  mapdunirnN  35130  mzpindd  35500  fiphp3d  35574  rencldnfilem  35575  irrapx1  35585  pellexlem3  35588  pellfundre  35642  pellfundge  35643  pellfundlb  35645  pellfundglb  35646  jm2.22  35763  jm2.23  35764  rpnnen3  35800  fglmod  35844  pwssplit4  35860  pwfi2f1o  35867  hbtlem6  35901  dgraalem  35920  dgraalemOLD  35921  dgraaub  35926  dgraaubOLD  35927  itgocn  35943  rgspncl  35948  phisum  35989  binomcxplemdvbinom  36615  binomcxplemcvg  36616  binomcxplemnotnn0  36618  uzwo4  37308  disjf1o  37370  limcperiod  37591  sumnnodd  37593  cncfshift  37634  cncfperiod  37639  ioodvbdlimc1lem1  37686  ioodvbdlimc1lem1OLD  37688  dvnprodlem1  37704  dvnprodlem2  37705  stoweidlem14  37757  stoweidlem34  37778  stoweidlem44  37788  stoweidlem50  37794  stoweidlem51  37795  stoweidlem52  37796  stoweidlem57  37801  stoweidlem59  37803  fourierdlem19  37871  fourierdlem20  37872  fourierdlem25  37877  fourierdlem31  37883  fourierdlem31OLD  37884  fourierdlem37  37890  fourierdlem42  37895  fourierdlem42OLD  37896  fourierdlem51  37904  fourierdlem54  37907  fourierdlem64  37917  fourierdlem79  37932  elaa2lem  37980  elaa2lemOLD  37981  etransclem16  37998  etransclem24  38006  etransclem31  38013  etransclem33  38015  etransclem34  38016  etransclem48OLD  38030  etransclem48  38031  salgencl  38054  meadjiunlem  38154  caragenss  38176  caratheodory  38200  ovnlecvr  38227  ovnsslelem  38229  ovnlerp  38231  ovn0lem  38234  ovnsubaddlem1  38239  hoidmv1lelem1  38260  hoidmv1lelem3  38262  hoidmvlelem1  38264  hoidmvlelem2  38265  hoidmvlelem3  38266  hoidmvlelem4  38267  ovnhoilem1  38270  ovnhoilem2  38271  perfectALTVlem2  38657  incistruhgr  38947  upgrss  38956  upgrn0  38957  upgruhgr  38967  usgrss  39026  uspgrushgr  39027  usgredgedga  39064  rabsubmgmd  39392  mgmhmeql  39404  oddibas  39414  2zlidl  39535  2zrngbas  39537  2zrng0  39539
  Copyright terms: Public domain W3C validator