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

Theorem ssrab2 3428
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 3427 . 2  |-  { x  |  ( x  e.  A  /\  ph ) }  C_  A
31, 2eqsstri 3378 1  |-  { x  e.  A  |  ph }  C_  A
Colors of variables: wff set class
Syntax hints:    /\ wa 359    e. wcel 1725   {cab 2422   {crab 2709    C_ wss 3320
This theorem is referenced by:  ssrabeq  3429  iinrab2  4154  riinrab  4166  rabexg  4353  pwnss  4365  frminex  4562  wereu2  4579  onminesb  4778  onminsb  4779  onintrab  4781  onnminsb  4784  onminex  4787  tfis  4834  omsson  4849  dmmptss  5366  ssimaex  5788  fnsuppres  5952  weniso  6075  canth  6539  riotacl  6564  riotassuni  6588  oawordeulem  6797  oeeulem  6844  nnawordex  6880  pmvalg  7029  fineqvlem  7323  ordtypelem2  7488  ordtypelem3  7489  ordtypelem4  7490  ordtypelem6  7492  hartogs  7513  wemapso2  7521  card2on  7522  wdom2d  7548  cantnfres  7633  oemapvali  7640  wemapwe  7654  tz9.12lem1  7713  tz9.12lem3  7715  rankf  7720  cplem1  7813  cardf2  7830  cardid2  7840  cardmin2  7885  acni3  7928  dfac2a  8010  cofsmo  8149  coftr  8153  fin2i2  8198  isfin2-2  8199  enfin2i  8201  fin23lem28  8220  fin23lem30  8222  isf32lem5  8237  isf32lem6  8238  isf32lem7  8239  isf32lem8  8240  fin1a2lem11  8290  fin1a2lem12  8291  hsmexlem4  8309  hsmexlem5  8310  hsmexlem6  8311  axdc3lem4  8333  ac6num  8359  ac6  8360  zorn2lem1  8376  zorn2lem3  8378  zorn2lem4  8379  zorn2lem5  8380  ondomon  8438  alephval2  8447  pwfseqlem1  8533  pwfseqlem3  8535  wunccl  8619  tskmcl  8716  0nnq  8801  elpqn  8802  infm3  9967  infmrcl  9987  uzf  10491  nnwos  10544  supminf  10563  zsupss  10565  rpnnen1lem1  10600  rpnnen1lem2  10601  rpnnen1lem3  10602  rpnnen1lem5  10604  rpre  10618  ixxf  10926  fzf  11047  flval3  11222  expge0  11416  expge1  11417  hashbclem  11701  sqrlem3  12050  sqrlem5  12052  rlimrege0  12373  incexc2  12618  divalglem2  12915  divalglem5  12917  divalglem8  12920  bitsf  12939  bitsfzolem  12946  sadadd2lem  12971  sadadd3  12973  sadcl  12974  smupf  12990  smuval2  12994  smupvallem  12995  smucl  12996  smueqlem  13002  gcdcllem3  13013  bezoutlem2  13039  bezoutlem3  13040  maxprmfct  13113  phicl2  13157  phibnd  13160  hashdvds  13164  phiprmpw  13165  phimullem  13168  eulerthlem2  13171  eulerth  13172  odzcllem  13178  odzdvds  13181  pclem  13212  infpn2  13281  prmreclem1  13284  prmreclem2  13285  prmreclem3  13286  prmreclem4  13287  prmreclem5  13288  4sqlem13  13325  4sqlem14  13326  4sqlem17  13329  4sqlem18  13330  vdwnnlem3  13365  hashbccl  13371  ramcl2lem  13377  ramtcl  13378  ramtcl2  13379  ramtub  13380  prdsds  13686  imasdsval2  13742  mrcflem  13831  isacs1i  13882  wunnat  14153  dmcoass  14221  lubid  14439  mhmeql  14764  gsumval1  14779  nmzsubg  14981  nmznsg  14984  conjnmz  15039  conjnmzb  15040  gastacl  15086  cntzval  15120  cntzssv  15127  odlem1  15173  odlem2  15177  odngen  15211  gexlem1  15213  gexlem2  15216  sylow1lem2  15233  sylow1lem3  15234  sylow1lem4  15235  sylow1lem5  15236  sylow2alem2  15252  sylow2a  15253  sylow2blem3  15256  sylow3lem2  15262  oddvdssubg  15470  cyggex2  15506  ablfacrplem  15623  ablfacrp2  15625  ablfac1eu  15631  pgpfaclem1  15639  ablfaclem2  15644  ablfaclem3  15645  lssacs  16043  lspf  16050  lspsolvlem  16214  lbsextlem2  16231  lbsextlem3  16232  lbsextlem4  16233  rrgeq0  16350  rrgss  16352  asplss  16388  aspsubrg  16390  psrbagconf1o  16439  psrass1lem  16442  psrdi  16470  psrdir  16471  psrass23  16473  resspsrmul  16480  mplbas  16493  mplbasss  16496  mplsubglem  16498  mplsubrglem  16502  mplmonmul  16527  psropprmul  16632  coe1mul2lem2  16661  cygznlem2a  16848  ocvfval  16893  ocvval  16894  fctop  17068  cctop  17070  ppttop  17071  epttop  17073  clscld  17111  mretopd  17156  neips  17177  neiptopnei  17196  ordtbaslem  17252  ordtuni  17254  ordtcld1  17261  ordtcld2  17262  cnpfval  17298  iscnp2  17303  cmpcov2  17453  cmpsublem  17462  tgcmp  17464  hauscmplem  17469  concompcld  17497  1stcfb  17508  2ndc1stc  17514  2ndcdisj  17519  kgentopon  17570  xkotf  17617  txkgen  17684  xkococnlem  17691  imastopn  17752  kqffn  17757  opnfbas  17874  flimfnfcls  18060  alexsubALT  18082  ptcmplem1  18083  ptcmplem2  18084  ptcmplem3  18085  symgtgp  18131  tgpconcompeqg  18141  tgpconcomp  18142  ghmcnp  18144  tsmsfbas  18157  eltsms  18162  utoptop  18264  utopbas  18265  imasdsf1olem  18403  blfvalps  18413  blfps  18436  blf  18437  blcld  18535  nmoffn  18745  nmofval  18748  nmogelb  18750  nmolb  18751  nmof  18753  icccmplem1  18853  icccmplem2  18854  icccmplem3  18855  ishtpy  18997  clsocv  19204  minveclem3b  19329  minveclem4  19333  ivthlem1  19348  ivthlem2  19349  ivthlem3  19350  ovolcl  19374  ovollb  19375  ovolgelb  19376  ovolge0  19377  ovolsslem  19380  ovolshftlem1  19405  ovolshft  19407  ovolscalem1  19409  ovolscalem2  19410  ovolsca  19411  ovolicc2lem3  19415  ovolicc2lem4  19416  ovolicc2lem5  19417  ovolicc2  19418  shftmbl  19433  iundisj  19442  dyadmax  19490  dyadmbllem  19491  dyadmbl  19492  opnmbllem  19493  iblmbf  19659  mdegmullem  20001  uc1pval  20062  mon1pval  20064  elqaalem1  20236  elqaalem3  20238  aannenlem2  20246  aalioulem2  20250  radcnvcl  20333  radcnvlt1  20334  radcnvle  20336  abelthlem4  20350  abelthlem6  20352  abelthlem9  20356  abelth  20357  atancn  20776  ftalem3  20857  ftalem4  20858  ftalem5  20859  efnnfsumcl  20885  isppw  20897  sgmval2  20926  efchtdvds  20942  sqff1o  20965  dvdsflip  20967  fsumdvdsdiaglem  20968  fsumdvdsdiag  20969  fsumdvdscom  20970  musum  20976  muinv  20978  dvdsmulf1o  20979  fsumdvdsmul  20980  sgmmul  20985  ppiub  20988  vmasum  21000  logfac2  21001  perfectlem2  21014  lgsfcl2  21086  lgsfcl  21088  lgscl  21094  lgseisenlem3  21135  lgseisenlem4  21136  lgsquadlem1  21138  lgsquadlem2  21139  rpvmasumlem  21181  rpvmasum2  21206  dchrisum0re  21207  dchrisum0lema  21208  dchrisum0lem1b  21209  dchrisum0lem1  21210  dchrisum0lem2a  21211  dchrisum0lem2  21212  dchrisum0lem3  21213  dchrisum0  21214  mudivsum  21224  mulogsum  21226  mulog2sumlem2  21229  vmalogdivsum2  21232  logsqvma  21236  logsqvma2  21237  selberglem3  21241  selberg  21242  selberg34r  21265  pntsval2  21270  pntrlog2bndlem1  21271  pntlem3  21303  umgrass  21354  umgran0  21355  umisuhgra  21362  usgrass  21384  usgrares1  21424  usgrafilem1  21425  nbgrassvt  21445  nbgraf1olem1  21451  cusgrares  21481  vdgrun  21672  vdgrfiun  21673  konigsberg  21709  ocsh  22785  spancl  22838  shsval2i  22889  ococin  22910  chsupid  22914  speccl  23402  atssch  23846  hatomistici  23865  chpssati  23866  iundisjf  24029  iundisjfi  24152  esumpinfval  24463  sigagensiga  24524  measvuni  24568  imambfm  24612  dya2iocuni  24633  ballotlemoex  24743  ballotlem2  24746  ballotlemfc0  24750  ballotlemfcc  24751  ballotlemfmpn  24752  ballotlemiex  24759  ballotlemsup  24762  ballotlem7  24793  ballotth  24795  lgamucov  24822  lgamucov2  24823  subfacp1lem3  24868  subfacp1lem5  24870  subfacp1lem6  24871  erdszelem2  24878  conpcon  24922  cvmliftmolem2  24969  cvmliftlem15  24985  cvmlift2lem12  25001  snmlff  25016  tfisg  25479  wfisg  25484  frinsg  25520  wlimss  25580  sltval2  25611  nodenselem4  25639  nobndlem5  25651  nofulllem5  25661  axcontlem2  25904  axcontlem7  25909  axcontlem8  25910  axcontlem10  25912  rankeq1o  26112  opnmbllem0  26242  mblfinlem1  26243  mblfinlem2  26244  ismblfin  26247  mbfposadd  26254  cnambfre  26255  finminlem  26321  fnessref  26373  finlocfin  26379  neibastop1  26388  neibastop2lem  26389  cover2  26415  indexa  26435  fdc  26449  sstotbnd2  26483  sstotbnd3  26485  igenidl  26673  prnc  26677  mzpindd  26803  fiphp3d  26880  rencldnfilem  26881  irrapx1  26891  pellexlem3  26894  pellfundre  26944  pellfundge  26945  pellfundlb  26947  pellfundglb  26948  jm2.22  27066  jm2.23  27067  rpnnen3  27103  fglmod  27148  pwssplit4  27168  dsmmbase  27178  dsmmval2  27179  dsmmsubg  27186  frlmsslsp  27225  pwfi2f1o  27237  hbtlem6  27310  dgraalem  27327  dgraaub  27330  itgocn  27346  rgspncl  27351  issubmd  27360  symgsssg  27385  symgfisg  27386  psgnghm  27414  phisum  27495  stoweidlem14  27739  stoweidlem34  27759  stoweidlem44  27769  stoweidlem50  27775  stoweidlem51  27776  stoweidlem52  27777  stoweidlem57  27782  stoweidlem59  27784  frisusgranb  28387  frgrawopreg1  28439  frgrawopreg2  28440  bnj21  29082  bnj110  29229  bnj1204  29381  bnj1311  29393  toycom  29770  lkrlss  29893  atlatmstc  30117  atlatle  30118  glbconN  30174  linepsubN  30549  pmapssat  30556  pmaple  30558  pmapsub  30565  paddssat  30611  diass  31840  diaglbN  31853  diaintclN  31856  diassdvaN  31858  docaclN  31922  dibglbN  31964  dibintclN  31965  diclspsn  31992  dihglblem2N  32092  dih1dimatlem  32127  dihglb2  32140  dochval2  32150  dochcl  32151  dochvalr  32155  doch2val2  32162  dochss  32163  dochocss  32164  lclkr  32331  lclkrs  32337  lcdvbase  32391  lcdvbasess  32392  mapdunirnN  32448
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rab 2714  df-in 3327  df-ss 3334
  Copyright terms: Public domain W3C validator