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

Theorem ssrab2 3425
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 2714 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
2 ssab2 3424 . 2  |-  { x  |  ( x  e.  A  /\  ph ) }  C_  A
31, 2eqsstri 3374 1  |-  { x  e.  A  |  ph }  C_  A
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    e. wcel 1755   {cab 2419   {crab 2709    C_ wss 3316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rab 2714  df-in 3323  df-ss 3330
This theorem is referenced by:  ssrabeq  3426  iinrab2  4221  riinrab  4234  rabexg  4430  pwnss  4445  frminex  4687  wereu2  4704  dmmptss  5322  ssimaex  5744  f1oresrab  5862  fnsuppresOLD  5925  weniso  6032  canth  6036  riotacl  6055  riotassuniOLD  6078  onminesb  6398  onminsb  6399  onintrab  6401  onnminsb  6404  onminex  6407  tfis  6454  omsson  6469  suppssdm  6692  fnsuppres  6705  oawordeulem  6981  oeeulem  7028  nnawordex  7064  pmvalg  7213  fineqvlem  7515  ordtypelem2  7721  ordtypelem3  7722  ordtypelem4  7723  ordtypelem6  7725  hartogs  7746  wemapso2OLD  7754  wemapso2lem  7755  card2on  7757  wdom2d  7783  oemapvali  7880  wemapwe  7916  wemapweOLD  7917  tz9.12lem1  7982  tz9.12lem3  7984  rankf  7989  cplem1  8084  cardf2  8101  cardid2  8111  cardmin2  8156  acni3  8205  dfac2a  8287  cofsmo  8426  coftr  8430  fin2i2  8475  isfin2-2  8476  enfin2i  8478  fin23lem28  8497  fin23lem30  8499  isf32lem5  8514  isf32lem6  8515  isf32lem7  8516  isf32lem8  8517  fin1a2lem11  8567  fin1a2lem12  8568  hsmexlem4  8586  hsmexlem5  8587  hsmexlem6  8588  axdc3lem4  8610  ac6num  8636  ac6  8637  zorn2lem1  8653  zorn2lem3  8655  zorn2lem4  8656  zorn2lem5  8657  ondomon  8715  alephval2  8724  pwfseqlem1  8813  pwfseqlem3  8815  wunccl  8899  tskmcl  8996  0nnq  9081  elpqn  9082  infm3  10277  infmrcl  10297  uzf  10852  nnwos  10910  supminf  10930  zsupss  10932  rpnnen1lem1  10967  rpnnen1lem2  10968  rpnnen1lem3  10969  rpnnen1lem5  10971  rpre  10985  ixxf  11298  fzf  11428  flval3  11647  expge0  11884  expge1  11885  hashbclem  12189  sqrlem3  12718  sqrlem5  12720  rlimrege0  13041  incexc2  13284  divalglem2  13582  divalglem5  13584  divalglem8  13587  bitsf  13606  bitsfzolem  13613  sadadd2lem  13638  sadadd3  13640  sadcl  13641  smupf  13657  smuval2  13661  smupvallem  13662  smucl  13663  smueqlem  13669  gcdcllem3  13680  bezoutlem2  13706  bezoutlem3  13707  maxprmfct  13782  phicl2  13826  phibnd  13829  hashdvds  13833  phiprmpw  13834  phimullem  13837  eulerthlem2  13840  eulerth  13841  odzcllem  13847  odzdvds  13850  pclem  13888  infpn2  13957  prmreclem1  13960  prmreclem2  13961  prmreclem3  13962  prmreclem4  13963  prmreclem5  13964  4sqlem13  14001  4sqlem14  14002  4sqlem17  14005  4sqlem18  14006  vdwnnlem3  14041  hashbccl  14047  ramcl2lem  14053  ramtcl  14054  ramtcl2  14055  ramtub  14056  prdsds  14385  imasdsval2  14437  mrcflem  14527  isacs1i  14578  wunnat  14849  dmcoass  14917  lublecl  15142  lubid  15143  issubmd  15459  mhmeql  15474  gsumval1  15489  nmzsubg  15702  nmznsg  15705  conjnmz  15760  conjnmzb  15761  gastacl  15807  cntzval  15819  cntzssv  15826  symgsssg  15953  symgfisg  15954  pmtrdifellem4  15965  odlem1  16018  odlem2  16022  odngen  16056  gexlem1  16058  gexlem2  16061  sylow1lem2  16078  sylow1lem3  16079  sylow1lem4  16080  sylow1lem5  16081  sylow2alem2  16097  sylow2a  16098  sylow2blem3  16101  sylow3lem2  16107  oddvdssubg  16317  cyggex2  16353  ablfacrplem  16540  ablfacrp2  16542  ablfac1eu  16548  pgpfaclem1  16556  ablfaclem2  16561  ablfaclem3  16562  lssacs  16970  lspf  16977  lspsolvlem  17145  lbsextlem2  17162  lbsextlem3  17163  lbsextlem4  17164  rrgeq0  17283  rrgss  17286  asplss  17322  aspsubrg  17324  psrbagconf1o  17378  psrass1lem  17381  psrdi  17413  psrdir  17414  psrass23  17416  resspsrmul  17423  mplbas  17437  mplbasOLD  17439  mplbasss  17442  mplsubglem  17444  mplsubglemOLD  17446  mplsubrglem  17451  mplsubrglemOLD  17452  mplmonmul  17477  psropprmul  17591  coe1mul2lem2  17620  cygznlem2a  17842  psgnghm  17852  ocvfval  17933  ocvval  17934  dsmmbase  18002  dsmmval2  18003  dsmmsubg  18010  frlmsslsp  18065  frlmsslspOLD  18066  smadiadet  18318  fctop  18450  cctop  18452  ppttop  18453  epttop  18455  clscld  18493  mretopd  18538  neips  18559  neiptopnei  18578  ordtbaslem  18634  ordtuni  18636  ordtcld1  18643  ordtcld2  18644  cnpfval  18680  iscnp2  18685  cmpcov2  18835  cmpsublem  18844  tgcmp  18846  hauscmplem  18851  concompcld  18880  1stcfb  18891  2ndc1stc  18897  2ndcdisj  18902  kgentopon  18953  xkotf  19000  txkgen  19067  xkococnlem  19074  imastopn  19135  kqffn  19140  opnfbas  19257  flimfnfcls  19443  alexsubALT  19465  ptcmplem1  19466  ptcmplem2  19467  ptcmplem3  19468  symgtgp  19514  tgpconcompeqg  19524  tgpconcomp  19525  ghmcnp  19527  tsmsfbas  19540  eltsms  19545  utoptop  19651  utopbas  19652  imasdsf1olem  19790  blfvalps  19800  blfps  19823  blf  19824  blcld  19922  nmoffn  20132  nmofval  20135  nmogelb  20137  nmolb  20138  nmof  20140  icccmplem1  20241  icccmplem2  20242  icccmplem3  20243  ishtpy  20386  clsocv  20604  rrxnm  20737  rrxf  20742  minveclem3b  20757  minveclem4  20761  ivthlem1  20777  ivthlem2  20778  ivthlem3  20779  ovolcl  20803  ovollb  20804  ovolgelb  20805  ovolge0  20806  ovolsslem  20809  ovolshftlem1  20834  ovolshft  20836  ovolscalem1  20838  ovolscalem2  20839  ovolsca  20840  ovolicc2lem3  20844  ovolicc2lem4  20845  ovolicc2lem5  20846  ovolicc2  20847  shftmbl  20862  iundisj  20871  dyadmax  20920  dyadmbllem  20921  dyadmbl  20922  opnmbllem  20923  iblmbf  21087  mdegmullem  21434  uc1pval  21496  mon1pval  21498  elqaalem1  21670  elqaalem3  21672  aannenlem2  21680  aalioulem2  21684  radcnvcl  21767  radcnvlt1  21768  radcnvle  21770  abelthlem4  21784  abelthlem6  21786  abelthlem9  21790  abelth  21791  atancn  22216  ftalem3  22297  ftalem4  22298  ftalem5  22299  efnnfsumcl  22325  isppw  22337  sgmval2  22366  efchtdvds  22382  sqff1o  22405  dvdsflip  22407  fsumdvdsdiaglem  22408  fsumdvdsdiag  22409  fsumdvdscom  22410  musum  22416  muinv  22418  dvdsmulf1o  22419  fsumdvdsmul  22420  sgmmul  22425  ppiub  22428  vmasum  22440  logfac2  22441  perfectlem2  22454  lgsfcl2  22526  lgsfcl  22528  lgscl  22534  lgsquadlem1  22578  lgsquadlem2  22579  rpvmasumlem  22621  rpvmasum2  22646  dchrisum0re  22647  dchrisum0lema  22648  dchrisum0lem1b  22649  dchrisum0lem1  22650  dchrisum0lem2a  22651  dchrisum0lem2  22652  dchrisum0lem3  22653  dchrisum0  22654  mudivsum  22664  mulogsum  22666  mulog2sumlem2  22669  vmalogdivsum2  22672  logsqvma  22676  logsqvma2  22677  selberglem3  22681  selberg  22682  selberg34r  22705  pntsval2  22710  pntrlog2bndlem1  22711  pntlem3  22743  tglnunirn  22863  tglnssp  22865  axcontlem2  23034  axcontlem7  23039  axcontlem8  23040  axcontlem10  23042  umgrass  23076  umgran0  23077  umisuhgra  23084  usgrass  23106  usgrares1  23146  usgrafilem1  23147  nbgrassvt  23167  nbgraf1olem1  23173  cusgrares  23203  vdgrun  23394  vdgrfiun  23395  konigsberg  23431  ocsh  24509  spancl  24562  shsval2i  24613  ococin  24634  chsupid  24638  speccl  25126  atssch  25570  hatomistici  25589  chpssati  25590  iundisjf  25755  fcobijfs  25850  fpwrelmap  25858  iundisjfi  25903  esumpinfval  26376  sigagensiga  26438  measvuni  26482  imambfm  26531  dya2iocuni  26552  oddpwdc  26585  eulerpartlem1  26598  eulerpartlemt  26602  eulerpartgbij  26603  eulerpartlemmf  26606  eulerpartlemgvv  26607  eulerpartlemgh  26609  eulerpartlemgs2  26611  ballotlemoex  26716  ballotlem2  26719  ballotlemfc0  26723  ballotlemfcc  26724  ballotlemfmpn  26725  ballotlemiex  26732  ballotlemsup  26735  ballotlem7  26766  ballotth  26768  lgamucov  26872  lgamucov2  26873  subfacp1lem3  26918  subfacp1lem5  26920  subfacp1lem6  26921  erdszelem2  26928  conpcon  26972  cvmliftmolem2  27019  cvmliftlem15  27035  cvmlift2lem12  27051  snmlff  27066  tfisg  27512  wfisg  27517  frinsg  27553  wlimss  27613  sltval2  27644  nodenselem4  27672  nobndlem5  27684  nofulllem5  27694  rankeq1o  28056  fin2so  28260  opnmbllem0  28271  mblfinlem1  28272  mblfinlem2  28273  ismblfin  28276  mbfposadd  28283  cnambfre  28284  finminlem  28357  fnessref  28409  finlocfin  28415  neibastop1  28424  neibastop2lem  28425  cover2  28451  indexa  28471  fdc  28485  sstotbnd2  28517  sstotbnd3  28519  igenidl  28707  prnc  28711  mzpindd  28927  fiphp3d  29003  rencldnfilem  29004  irrapx1  29014  pellexlem3  29017  pellfundre  29067  pellfundge  29068  pellfundlb  29070  pellfundglb  29071  jm2.22  29189  jm2.23  29190  rpnnen3  29226  fglmod  29271  pwssplit4  29287  pwfi2f1o  29296  hbtlem6  29330  dgraalem  29347  dgraaub  29350  itgocn  29366  rgspncl  29371  phisum  29412  stoweidlem14  29655  stoweidlem34  29675  stoweidlem44  29685  stoweidlem50  29691  stoweidlem51  29692  stoweidlem52  29693  stoweidlem57  29698  stoweidlem59  29700  clwwlksswrd  30286  hashwwlkext  30411  frisusgranb  30435  frgrawopreg1  30489  frgrawopreg2  30490  bnj21  31408  bnj110  31553  bnj1204  31705  bnj1311  31717  bj-rabtr  32018  bj-rabtrAUTO  32020  bj-vecmod  32152  bj-rrvecvec  32162  toycom  32191  lkrlss  32313  atlatmstc  32537  atlatle  32538  glbconN  32594  linepsubN  32969  pmapssat  32976  pmaple  32978  pmapsub  32985  paddssat  33031  diass  34260  diaglbN  34273  diaintclN  34276  diassdvaN  34278  docaclN  34342  dibglbN  34384  dibintclN  34385  diclspsn  34412  dihglblem2N  34512  dih1dimatlem  34547  dihglb2  34560  dochval2  34570  dochcl  34571  dochvalr  34575  doch2val2  34582  dochss  34583  dochocss  34584  lclkr  34751  lclkrs  34757  lcdvbase  34811  lcdvbasess  34812  mapdunirnN  34868
  Copyright terms: Public domain W3C validator