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

Theorem ssrab2 3546
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 2808 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
2 ssab2 3545 . 2  |-  { x  |  ( x  e.  A  /\  ph ) }  C_  A
31, 2eqsstri 3495 1  |-  { x  e.  A  |  ph }  C_  A
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    e. wcel 1758   {cab 2439   {crab 2803    C_ wss 3437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2808  df-in 3444  df-ss 3451
This theorem is referenced by:  ssrabeq  3547  iinrab2  4342  riinrab  4355  rabexg  4551  pwnss  4566  frminex  4809  wereu2  4826  dmmptss  5443  ssimaex  5866  f1oresrab  5985  fnsuppresOLD  6048  weniso  6155  canth  6159  riotacl  6177  riotassuniOLD  6199  onminesb  6520  onminsb  6521  onintrab  6523  onnminsb  6526  onminex  6529  tfis  6576  omsson  6591  suppssdm  6814  fnsuppres  6827  oawordeulem  7104  oeeulem  7151  nnawordex  7187  pmvalg  7336  fineqvlem  7639  ordtypelem2  7845  ordtypelem3  7846  ordtypelem4  7847  ordtypelem6  7849  hartogs  7870  wemapso2OLD  7878  wemapso2lem  7879  card2on  7881  wdom2d  7907  oemapvali  8004  wemapwe  8040  wemapweOLD  8041  tz9.12lem1  8106  tz9.12lem3  8108  rankf  8113  cplem1  8208  cardf2  8225  cardid2  8235  cardmin2  8280  acni3  8329  dfac2a  8411  cofsmo  8550  coftr  8554  fin2i2  8599  isfin2-2  8600  enfin2i  8602  fin23lem28  8621  fin23lem30  8623  isf32lem5  8638  isf32lem6  8639  isf32lem7  8640  isf32lem8  8641  fin1a2lem11  8691  fin1a2lem12  8692  hsmexlem4  8710  hsmexlem5  8711  hsmexlem6  8712  axdc3lem4  8734  ac6num  8760  ac6  8761  zorn2lem1  8777  zorn2lem3  8779  zorn2lem4  8780  zorn2lem5  8781  ondomon  8839  alephval2  8848  pwfseqlem1  8937  pwfseqlem3  8939  wunccl  9023  tskmcl  9120  0nnq  9205  elpqn  9206  infm3  10401  infmrcl  10421  uzf  10976  nnwos  11034  supminf  11054  zsupss  11056  rpnnen1lem1  11091  rpnnen1lem2  11092  rpnnen1lem3  11093  rpnnen1lem5  11095  rpre  11109  ixxf  11422  fzf  11559  flval3  11781  expge0  12018  expge1  12019  hashbclem  12324  sqrlem3  12853  sqrlem5  12855  rlimrege0  13176  incexc2  13420  divalglem2  13718  divalglem5  13720  divalglem8  13723  bitsf  13742  bitsfzolem  13749  sadadd2lem  13774  sadadd3  13776  sadcl  13777  smupf  13793  smuval2  13797  smupvallem  13798  smucl  13799  smueqlem  13805  gcdcllem3  13816  bezoutlem2  13842  bezoutlem3  13843  maxprmfct  13918  phicl2  13962  phibnd  13965  hashdvds  13969  phiprmpw  13970  phimullem  13973  eulerthlem2  13976  eulerth  13977  odzcllem  13983  odzdvds  13986  pclem  14024  infpn2  14093  prmreclem1  14096  prmreclem2  14097  prmreclem3  14098  prmreclem4  14099  prmreclem5  14100  4sqlem13  14137  4sqlem14  14138  4sqlem17  14141  4sqlem18  14142  vdwnnlem3  14177  hashbccl  14183  ramcl2lem  14189  ramtcl  14190  ramtcl2  14191  ramtub  14192  prdsds  14522  imasdsval2  14574  mrcflem  14664  isacs1i  14715  wunnat  14986  dmcoass  15054  lublecl  15279  lubid  15280  issubmd  15597  mhmeql  15612  gsumval1  15629  nmzsubg  15842  nmznsg  15845  conjnmz  15900  conjnmzb  15901  gastacl  15947  cntzval  15959  cntzssv  15966  symgsssg  16093  symgfisg  16094  pmtrdifellem4  16105  odlem1  16160  odlem2  16164  odngen  16198  gexlem1  16200  gexlem2  16203  sylow1lem2  16220  sylow1lem3  16221  sylow1lem4  16222  sylow1lem5  16223  sylow2alem2  16239  sylow2a  16240  sylow2blem3  16243  sylow3lem2  16249  oddvdssubg  16459  cyggex2  16495  ablfacrplem  16689  ablfacrp2  16691  ablfac1eu  16697  pgpfaclem1  16705  ablfaclem2  16710  ablfaclem3  16711  lssacs  17172  lspf  17179  lspsolvlem  17347  lbsextlem2  17364  lbsextlem3  17365  lbsextlem4  17366  rrgeq0  17485  rrgss  17488  asplss  17524  aspsubrg  17526  psrbagconf1o  17568  psrass1lem  17571  psrdi  17603  psrdir  17604  psrass23l  17605  psrass23  17607  resspsrmul  17614  mplbas  17628  mplbasOLD  17630  mplbasss  17633  mplsubglem  17635  mplsubglemOLD  17637  mplsubrglem  17642  mplsubrglemOLD  17643  mplmonmul  17668  psropprmul  17817  coe1mul2lem2  17846  cygznlem2a  18126  psgnghm  18136  ocvfval  18217  ocvval  18218  dsmmbase  18286  dsmmval2  18287  dsmmsubg  18294  frlmsslsp  18349  frlmsslspOLD  18350  smadiadet  18609  fctop  18741  cctop  18743  ppttop  18744  epttop  18746  clscld  18784  mretopd  18829  neips  18850  neiptopnei  18869  ordtbaslem  18925  ordtuni  18927  ordtcld1  18934  ordtcld2  18935  cnpfval  18971  iscnp2  18976  cmpcov2  19126  cmpsublem  19135  tgcmp  19137  hauscmplem  19142  concompcld  19171  1stcfb  19182  2ndc1stc  19188  2ndcdisj  19193  kgentopon  19244  xkotf  19291  txkgen  19358  xkococnlem  19365  imastopn  19426  kqffn  19431  opnfbas  19548  flimfnfcls  19734  alexsubALT  19756  ptcmplem1  19757  ptcmplem2  19758  ptcmplem3  19759  symgtgp  19805  tgpconcompeqg  19815  tgpconcomp  19816  ghmcnp  19818  tsmsfbas  19831  eltsms  19836  utoptop  19942  utopbas  19943  imasdsf1olem  20081  blfvalps  20091  blfps  20114  blf  20115  blcld  20213  nmoffn  20423  nmofval  20426  nmogelb  20428  nmolb  20429  nmof  20431  icccmplem1  20532  icccmplem2  20533  icccmplem3  20534  ishtpy  20677  clsocv  20895  rrxnm  21028  rrxf  21033  minveclem3b  21048  minveclem4  21052  ivthlem1  21068  ivthlem2  21069  ivthlem3  21070  ovolcl  21094  ovollb  21095  ovolgelb  21096  ovolge0  21097  ovolsslem  21100  ovolshftlem1  21125  ovolshft  21127  ovolscalem1  21129  ovolscalem2  21130  ovolsca  21131  ovolicc2lem3  21135  ovolicc2lem4  21136  ovolicc2lem5  21137  ovolicc2  21138  shftmbl  21154  iundisj  21163  dyadmax  21212  dyadmbllem  21213  dyadmbl  21214  opnmbllem  21215  iblmbf  21379  mdegmullem  21683  uc1pval  21745  mon1pval  21747  elqaalem1  21919  elqaalem3  21921  aannenlem2  21929  aalioulem2  21933  radcnvcl  22016  radcnvlt1  22017  radcnvle  22019  abelthlem4  22033  abelthlem6  22035  abelthlem9  22039  abelth  22040  atancn  22465  ftalem3  22546  ftalem4  22547  ftalem5  22548  efnnfsumcl  22574  isppw  22586  sgmval2  22615  efchtdvds  22631  sqff1o  22654  dvdsflip  22656  fsumdvdsdiaglem  22657  fsumdvdsdiag  22658  fsumdvdscom  22659  musum  22665  muinv  22667  dvdsmulf1o  22668  fsumdvdsmul  22669  sgmmul  22674  ppiub  22677  vmasum  22689  logfac2  22690  perfectlem2  22703  lgsfcl2  22775  lgsfcl  22777  lgscl  22783  lgsquadlem1  22827  lgsquadlem2  22828  rpvmasumlem  22870  rpvmasum2  22895  dchrisum0re  22896  dchrisum0lema  22897  dchrisum0lem1b  22898  dchrisum0lem1  22899  dchrisum0lem2a  22900  dchrisum0lem2  22901  dchrisum0lem3  22902  dchrisum0  22903  mudivsum  22913  mulogsum  22915  mulog2sumlem2  22918  vmalogdivsum2  22921  logsqvma  22925  logsqvma2  22926  selberglem3  22930  selberg  22931  selberg34r  22954  pntsval2  22959  pntrlog2bndlem1  22960  pntlem3  22992  tglnunirn  23119  tglnssp  23123  axcontlem2  23364  axcontlem7  23369  axcontlem8  23370  axcontlem10  23372  umgrass  23406  umgran0  23407  umisuhgra  23414  usgrass  23436  usgrares1  23476  usgrafilem1  23477  nbgrassvt  23497  nbgraf1olem1  23503  cusgrares  23533  vdgrun  23724  vdgrfiun  23725  konigsberg  23761  ocsh  24839  spancl  24892  shsval2i  24943  ococin  24964  chsupid  24968  speccl  25456  atssch  25900  hatomistici  25919  chpssati  25920  iundisjf  26083  fcobijfs  26178  fpwrelmap  26185  iundisjfi  26226  esumpinfval  26668  sigagensiga  26730  measvuni  26774  imambfm  26822  dya2iocuni  26843  oms0  26855  omsmon  26856  oddpwdc  26882  eulerpartlem1  26895  eulerpartlemt  26899  eulerpartgbij  26900  eulerpartlemmf  26903  eulerpartlemgvv  26904  eulerpartlemgh  26906  eulerpartlemgs2  26908  ballotlemoex  27013  ballotlem2  27016  ballotlemfc0  27020  ballotlemfcc  27021  ballotlemfmpn  27022  ballotlemiex  27029  ballotlemsup  27032  ballotlem7  27063  ballotth  27065  lgamucov  27169  lgamucov2  27170  subfacp1lem3  27215  subfacp1lem5  27217  subfacp1lem6  27218  erdszelem2  27225  conpcon  27269  cvmliftmolem2  27316  cvmliftlem15  27332  cvmlift2lem12  27348  snmlff  27363  tfisg  27810  wfisg  27815  frinsg  27851  wlimss  27911  sltval2  27942  nodenselem4  27970  nobndlem5  27982  nofulllem5  27992  rankeq1o  28354  fin2so  28565  opnmbllem0  28576  mblfinlem1  28577  mblfinlem2  28578  ismblfin  28581  mbfposadd  28588  cnambfre  28589  finminlem  28662  fnessref  28714  finlocfin  28720  neibastop1  28729  neibastop2lem  28730  cover2  28756  indexa  28776  fdc  28790  sstotbnd2  28822  sstotbnd3  28824  igenidl  29012  prnc  29016  mzpindd  29231  fiphp3d  29307  rencldnfilem  29308  irrapx1  29318  pellexlem3  29321  pellfundre  29371  pellfundge  29372  pellfundlb  29374  pellfundglb  29375  jm2.22  29493  jm2.23  29494  rpnnen3  29530  fglmod  29575  pwssplit4  29591  pwfi2f1o  29600  hbtlem6  29634  dgraalem  29651  dgraaub  29654  itgocn  29670  rgspncl  29675  phisum  29716  stoweidlem14  29958  stoweidlem34  29978  stoweidlem44  29988  stoweidlem50  29994  stoweidlem51  29995  stoweidlem52  29996  stoweidlem57  30001  stoweidlem59  30003  clwwlksswrd  30589  hashwwlkext  30714  frisusgranb  30738  frgrawopreg1  30792  frgrawopreg2  30793  rabssnn0fi  30896  dmatsgrp  31058  scmatsgrp  31065  pmatcoe1fsupp  31193  cpmatsubgpmat  31210  bnj21  32039  bnj110  32184  bnj1204  32336  bnj1311  32348  bj-rabtr  32765  bj-rabtrAUTO  32767  bj-cmnssmnd  32911  bj-vecssmod  32918  bj-rrvecssvec  32925  toycom  32957  lkrlss  33079  atlatmstc  33303  atlatle  33304  glbconN  33360  linepsubN  33735  pmapssat  33742  pmaple  33744  pmapsub  33751  paddssat  33797  diass  35026  diaglbN  35039  diaintclN  35042  diassdvaN  35044  docaclN  35108  dibglbN  35150  dibintclN  35151  diclspsn  35178  dihglblem2N  35278  dih1dimatlem  35313  dihglb2  35326  dochval2  35336  dochcl  35337  dochvalr  35341  doch2val2  35348  dochss  35349  dochocss  35350  lclkr  35517  lclkrs  35523  lcdvbase  35577  lcdvbasess  35578  mapdunirnN  35634
  Copyright terms: Public domain W3C validator