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

Theorem ssrab2 3258
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 2552 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
2 ssab2 3257 . 2  |-  { x  |  ( x  e.  A  /\  ph ) }  C_  A
31, 2eqsstri 3208 1  |-  { x  e.  A  |  ph }  C_  A
Colors of variables: wff set class
Syntax hints:    /\ wa 358    e. wcel 1684   {cab 2269   {crab 2547    C_ wss 3152
This theorem is referenced by:  iinrab2  3965  riinrab  3977  rabexg  4164  pwnss  4176  frminex  4373  wereu2  4390  onminesb  4589  onminsb  4590  onintrab  4592  onnminsb  4595  onminex  4598  tfis  4645  omsson  4660  dmmptss  5169  ssimaex  5584  fnsuppres  5732  weniso  5852  canth  6294  riotacl  6319  riotassuni  6343  oawordeulem  6552  oeeulem  6599  nnawordex  6635  pmvalg  6783  fineqvlem  7077  ordtypelem2  7234  ordtypelem3  7235  ordtypelem4  7236  ordtypelem6  7238  hartogs  7259  wemapso2  7267  card2on  7268  wdom2d  7294  cantnfres  7379  oemapvali  7386  wemapwe  7400  tz9.12lem1  7459  tz9.12lem3  7461  rankf  7466  cplem1  7559  cardf2  7576  cardid2  7586  cardmin2  7631  acni3  7674  dfac2a  7756  kmlem1  7776  cofsmo  7895  coftr  7899  fin2i2  7944  isfin2-2  7945  enfin2i  7947  fin23lem28  7966  fin23lem30  7968  isf32lem5  7983  isf32lem6  7984  isf32lem7  7985  isf32lem8  7986  fin1a2lem9  8034  fin1a2lem11  8036  fin1a2lem12  8037  hsmexlem4  8055  hsmexlem5  8056  hsmexlem6  8057  axdc3lem4  8079  ac6num  8106  ac6  8107  zorn2lem1  8123  zorn2lem3  8125  zorn2lem4  8126  zorn2lem5  8127  ondomon  8185  alephval2  8194  pwfseqlem1  8280  pwfseqlem3  8282  wunccl  8366  tskmcl  8463  0nnq  8548  elpqn  8549  infm3  9713  infmrcl  9733  nnind  9764  uzf  10233  nnwos  10286  ublbneg  10302  supminf  10305  zsupss  10307  rpnnen1lem1  10342  rpnnen1lem2  10343  rpnnen1lem3  10344  rpnnen1lem5  10346  rpre  10360  ixxf  10666  fzf  10786  flval3  10945  expge0  11138  expge1  11139  hashbclem  11390  sqrlem3  11730  sqrlem5  11732  rlimrege0  12053  incexc2  12297  divalglem2  12594  divalglem5  12596  divalglem8  12599  bitsf  12618  bitsfzolem  12625  sadadd2lem  12650  sadadd3  12652  sadcl  12653  smupf  12669  smuval2  12673  smupvallem  12674  smucl  12675  smueqlem  12681  gcdcllem3  12692  bezoutlem2  12718  bezoutlem3  12719  maxprmfct  12792  phicl2  12836  phibnd  12839  hashdvds  12843  phiprmpw  12844  phimullem  12847  eulerthlem2  12850  eulerth  12851  odzcllem  12857  odzdvds  12860  pclem  12891  infpn2  12960  prmreclem1  12963  prmreclem2  12964  prmreclem3  12965  prmreclem4  12966  prmreclem5  12967  4sqlem13  13004  4sqlem14  13005  4sqlem17  13008  4sqlem18  13009  vdwnnlem3  13044  hashbccl  13050  ramcl2lem  13056  ramtcl  13057  ramtcl2  13058  ramtub  13059  prdsds  13363  imasdsval2  13419  mrcflem  13508  isacs1i  13559  wunnat  13830  dmcoass  13898  lubid  14116  mhmeql  14441  gsumval1  14456  nmzsubg  14658  nmznsg  14661  conjnmz  14716  conjnmzb  14717  gastacl  14763  cntzval  14797  cntzssv  14804  odlem1  14850  odcl  14851  odlem2  14854  odngen  14888  gexlem1  14890  gexcl  14891  gexlem2  14893  gexdvds  14895  sylow1lem2  14910  sylow1lem3  14911  sylow1lem4  14912  sylow1lem5  14913  pgpssslw  14925  sylow2alem2  14929  sylow2a  14930  sylow2blem3  14933  sylow3lem2  14939  oddvdssubg  15147  cyggex2  15183  ablfacrplem  15300  ablfacrp2  15302  ablfac1eu  15308  pgpfaclem1  15316  ablfaclem2  15321  ablfaclem3  15322  lssacs  15724  lspf  15731  lspsolvlem  15895  lbsextlem2  15912  lbsextlem3  15913  lbsextlem4  15914  rrgeq0  16031  rrgss  16033  asplss  16069  aspsubrg  16071  psrbagconf1o  16120  psrass1lem  16123  psrdi  16151  psrdir  16152  psrass23  16154  resspsrmul  16161  mplbas  16174  mplbasss  16177  mplsubglem  16179  mplsubrglem  16183  mplmonmul  16208  psropprmul  16316  coe1mul2lem2  16345  coe1mul2  16346  cygznlem2a  16521  ocvfval  16566  ocvval  16567  fctop  16741  cctop  16743  ppttop  16744  epttop  16746  clscld  16784  mretopd  16829  neips  16850  ordtbaslem  16918  ordtuni  16920  ordtcld1  16927  ordtcld2  16928  cnpfval  16964  iscnp2  16969  cmpcov2  17117  cmpsublem  17126  tgcmp  17128  hauscmplem  17133  concompcld  17160  1stcfb  17171  2ndc1stc  17177  2ndcdisj  17182  kgentopon  17233  xkotf  17280  txkgen  17346  xkococnlem  17353  imastopn  17411  kqffn  17416  opnfbas  17537  flimfnfcls  17723  alexsubALT  17745  ptcmplem1  17746  ptcmplem2  17747  ptcmplem3  17748  symgtgp  17784  tgpconcompeqg  17794  tgpconcomp  17795  ghmcnp  17797  tsmsfbas  17810  eltsms  17815  imasdsf1olem  17937  blfval  17947  blf  17961  blcld  18051  nmoffn  18220  nmofval  18223  nmogelb  18225  nmolb  18226  nmof  18228  icccmplem1  18327  icccmplem2  18328  icccmplem3  18329  ishtpy  18470  clsocv  18677  minveclem3b  18792  minveclem4  18796  ivthlem1  18811  ivthlem2  18812  ivthlem3  18813  ovolcl  18837  ovollb  18838  ovolgelb  18839  ovolge0  18840  ovolsslem  18843  ovolshftlem1  18868  ovolshft  18870  ovolscalem1  18872  ovolscalem2  18873  ovolsca  18874  ovolicc2lem3  18878  ovolicc2lem4  18879  ovolicc2lem5  18880  ovolicc2  18881  shftmbl  18896  iundisj  18905  dyadmax  18953  dyadmbllem  18954  dyadmbl  18955  opnmbllem  18956  iblmbf  19122  mdegmullem  19464  uc1pval  19525  mon1pval  19527  elqaalem1  19699  elqaalem3  19701  aannenlem2  19709  aalioulem2  19713  radcnvcl  19793  radcnvlt1  19794  radcnvle  19796  abelthlem4  19810  abelthlem6  19812  abelthlem9  19816  abelth  19817  atancn  20232  ftalem3  20312  ftalem4  20313  ftalem5  20314  efnnfsumcl  20340  isppw  20352  sgmval2  20381  0sgm  20382  sgmf  20383  sgmnncl  20385  efchtdvds  20397  sqff1o  20420  dvdsflip  20422  fsumdvdsdiaglem  20423  fsumdvdsdiag  20424  fsumdvdscom  20425  dvdsppwf1o  20426  musum  20431  musumsum  20432  muinv  20433  dvdsmulf1o  20434  fsumdvdsmul  20435  sgmppw  20436  sgmmul  20440  ppiub  20443  vmasum  20455  logfac2  20456  perfectlem2  20469  lgsfcl2  20541  lgsfcl  20543  lgscl  20549  lgseisenlem3  20590  lgseisenlem4  20591  lgsquadlem1  20593  lgsquadlem2  20594  rpvmasumlem  20636  dchrmusum2  20643  dchrvmasumlem1  20644  dchrvmasum2lem  20645  dchrisum0fmul  20655  dchrisum0ff  20656  dchrisum0flblem1  20657  rpvmasum2  20661  dchrisum0re  20662  dchrisum0lema  20663  dchrisum0lem1b  20664  dchrisum0lem1  20665  dchrisum0lem2a  20666  dchrisum0lem2  20667  dchrisum0lem3  20668  dchrisum0  20669  mudivsum  20679  mulogsum  20681  mulog2sumlem2  20684  vmalogdivsum2  20687  logsqvma  20691  logsqvma2  20692  selberglem3  20696  selberg  20697  selberg34r  20720  pntsval2  20725  pntrlog2bndlem1  20726  pntlem3  20758  ocsh  21862  spancl  21915  shsval2i  21966  ococin  21987  chsupid  21991  speccl  22479  atssch  22923  hatomistici  22942  chpssati  22943  ballotlemoex  23044  ballotlem2  23047  ballotlemfc0  23051  ballotlemfcc  23052  ballotlemfmpn  23053  ballotlemiex  23060  ballotlemsup  23063  ballotlemirc  23090  ballotlem7  23094  ballotth  23096  iundisjfi  23363  iundisjf  23365  esumpinfval  23441  sigagensiga  23502  measvuni  23542  imambfm  23567  subfacp1lem3  23713  subfacp1lem5  23715  subfacp1lem6  23716  erdszelem2  23723  conpcon  23766  cvmliftmolem2  23813  cvmliftlem15  23829  cvmlift2lem12  23845  umgrass  23871  umgran0  23872  vdgrf  23891  vdgrun  23893  konigsberg  23911  snmlff  23912  tfisg  24204  wfisg  24209  frinsg  24245  sltval2  24310  nodenselem4  24338  nobndlem5  24350  nofulllem5  24360  axcontlem2  24593  axcontlem7  24598  axcontlem8  24599  axcontlem10  24601  rankeq1o  24801  ump  25046  dstr  25171  prtoptop  25549  usptop  25550  finminlem  26231  fnessref  26293  finptfin  26297  finlocfin  26299  neibastop1  26308  neibastop2lem  26309  cover2  26358  indexa  26412  fdc  26455  sstotbnd2  26498  sstotbnd3  26500  igenidl  26688  prnc  26692  mzpindd  26824  fiphp3d  26902  rencldnfilem  26903  irrapx1  26913  pellexlem3  26916  pellfundre  26966  pellfundge  26967  pellfundlb  26969  pellfundglb  26970  jm2.22  27088  jm2.23  27089  rpnnen3  27125  fglmod  27171  pwssplit4  27191  dsmmbase  27201  dsmmval2  27202  dsmmsubg  27209  frlmsslsp  27248  pwfi2f1o  27260  hbtlem6  27333  dgraalem  27350  dgraaub  27353  itgocn  27369  rgspncl  27374  issubmd  27383  symgsssg  27408  symgfisg  27409  psgnghm  27437  phisum  27518  stoweidlem14  27763  stoweidlem15  27764  stoweidlem34  27783  stoweidlem44  27793  stoweidlem50  27799  stoweidlem51  27800  stoweidlem52  27801  stoweidlem57  27806  stoweidlem59  27808  usgrass  28110  nbgrassvt  28148  bnj21  28743  bnj110  28890  bnj1204  29042  bnj1311  29054  toycom  29162  lkrlss  29285  atlatmstc  29509  atlatle  29510  glbconN  29566  linepsubN  29941  pmapssat  29948  pmaple  29950  pmapsub  29957  paddssat  30003  diass  31232  diaglbN  31245  diaintclN  31248  diassdvaN  31250  docaclN  31314  dibglbN  31356  dibintclN  31357  diclspsn  31384  dihglblem2N  31484  dih1dimatlem  31519  dihglb2  31532  dochval2  31542  dochcl  31543  dochvalr  31547  doch2val2  31554  dochss  31555  dochocss  31556  lclkr  31723  lclkrs  31729  lcdvbase  31783  lcdvbasess  31784  mapdunirnN  31840
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator