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

Theorem ssrab2 3585
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 2823 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
2 ssab2 3584 . 2  |-  { x  |  ( x  e.  A  /\  ph ) }  C_  A
31, 2eqsstri 3534 1  |-  { x  e.  A  |  ph }  C_  A
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    e. wcel 1767   {cab 2452   {crab 2818    C_ wss 3476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-in 3483  df-ss 3490
This theorem is referenced by:  ssrabeq  3586  iinrab2  4388  riinrab  4401  rabexg  4597  pwnss  4612  frminex  4859  wereu2  4876  dmmptss  5501  ssimaex  5930  f1oresrab  6051  fnsuppresOLD  6119  weniso  6236  canth  6240  riotacl  6258  riotassuniOLD  6280  onminesb  6611  onminsb  6612  onintrab  6614  onnminsb  6617  onminex  6620  tfis  6667  omsson  6682  suppssdm  6911  fnsuppres  6924  oawordeulem  7200  oeeulem  7247  nnawordex  7283  pmvalg  7428  fineqvlem  7731  ordtypelem2  7940  ordtypelem3  7941  ordtypelem4  7942  ordtypelem6  7944  hartogs  7965  wemapso2OLD  7973  wemapso2lem  7974  card2on  7976  wdom2d  8002  oemapvali  8099  wemapwe  8135  wemapweOLD  8136  tz9.12lem1  8201  tz9.12lem3  8203  rankf  8208  cplem1  8303  cardf2  8320  cardid2  8330  cardmin2  8375  acni3  8424  dfac2a  8506  cofsmo  8645  coftr  8649  fin2i2  8694  isfin2-2  8695  enfin2i  8697  fin23lem28  8716  fin23lem30  8718  isf32lem5  8733  isf32lem6  8734  isf32lem7  8735  isf32lem8  8736  fin1a2lem11  8786  fin1a2lem12  8787  hsmexlem4  8805  hsmexlem5  8806  hsmexlem6  8807  axdc3lem4  8829  ac6num  8855  ac6  8856  zorn2lem1  8872  zorn2lem3  8874  zorn2lem4  8875  zorn2lem5  8876  ondomon  8934  alephval2  8943  pwfseqlem1  9032  pwfseqlem3  9034  wunccl  9118  tskmcl  9215  0nnq  9298  elpqn  9299  infm3  10498  infmrcl  10518  uzf  11081  nnwos  11145  supminf  11165  zsupss  11167  rpnnen1lem1  11204  rpnnen1lem2  11205  rpnnen1lem3  11206  rpnnen1lem5  11208  rpre  11222  ixxf  11535  fzf  11672  flval3  11915  rabssnn0fi  12059  expge0  12166  expge1  12167  hashbclem  12463  sqrlem3  13037  sqrlem5  13039  rlimrege0  13361  incexc2  13609  divalglem2  13908  divalglem5  13910  divalglem8  13913  bitsf  13932  bitsfzolem  13939  sadadd2lem  13964  sadadd3  13966  sadcl  13967  smupf  13983  smuval2  13987  smupvallem  13988  smucl  13989  smueqlem  13995  gcdcllem3  14006  bezoutlem2  14032  bezoutlem3  14033  maxprmfct  14109  phicl2  14153  phibnd  14156  hashdvds  14160  phiprmpw  14161  phimullem  14164  eulerthlem2  14167  eulerth  14168  odzcllem  14174  odzdvds  14177  pclem  14217  infpn2  14286  prmreclem1  14289  prmreclem2  14290  prmreclem3  14291  prmreclem4  14292  prmreclem5  14293  4sqlem13  14330  4sqlem14  14331  4sqlem17  14334  4sqlem18  14335  vdwnnlem3  14370  hashbccl  14376  ramcl2lem  14382  ramtcl  14383  ramtcl2  14384  ramtub  14385  prdsds  14715  imasdsval2  14767  mrcflem  14857  isacs1i  14908  wunnat  15179  dmcoass  15247  lublecl  15472  lubid  15473  issubmd  15790  mhmeql  15805  gsumval1  15822  nmzsubg  16037  nmznsg  16040  conjnmz  16095  conjnmzb  16096  gastacl  16142  cntzval  16154  cntzssv  16161  symgsssg  16288  symgfisg  16289  pmtrdifellem4  16300  odlem1  16355  odlem2  16359  odngen  16393  gexlem1  16395  gexlem2  16398  sylow1lem2  16415  sylow1lem3  16416  sylow1lem4  16417  sylow1lem5  16418  sylow2alem2  16434  sylow2a  16435  sylow2blem3  16438  sylow3lem2  16444  oddvdssubg  16654  cyggex2  16690  ablfacrplem  16906  ablfacrp2  16908  ablfac1eu  16914  pgpfaclem1  16922  ablfaclem2  16927  ablfaclem3  16928  lssacs  17396  lspf  17403  lspsolvlem  17571  lbsextlem2  17588  lbsextlem3  17589  lbsextlem4  17590  rrgeq0  17709  rrgss  17712  asplss  17749  aspsubrg  17751  psrbagconf1o  17797  psrass1lem  17800  psrdi  17832  psrdir  17833  psrass23l  17834  psrass23  17836  resspsrmul  17843  mplbas  17857  mplbasOLD  17859  mplbasss  17862  mplsubglem  17864  mplsubglemOLD  17866  mplsubrglem  17871  mplsubrglemOLD  17872  mplmonmul  17897  psropprmul  18050  coe1mul2lem2  18080  cygznlem2a  18373  psgnghm  18383  ocvfval  18464  ocvval  18465  dsmmbase  18533  dsmmval2  18534  dsmmsubg  18541  frlmsslsp  18596  frlmsslspOLD  18597  scmatlss  18794  smadiadet  18939  pmatcoe1fsupp  18969  cpmatsubgpmat  18988  fctop  19271  cctop  19273  ppttop  19274  epttop  19276  clscld  19314  mretopd  19359  neips  19380  neiptopnei  19399  ordtbaslem  19455  ordtuni  19457  ordtcld1  19464  ordtcld2  19465  cnpfval  19501  iscnp2  19506  cmpcov2  19656  cmpsublem  19665  tgcmp  19667  hauscmplem  19672  concompcld  19701  1stcfb  19712  2ndc1stc  19718  2ndcdisj  19723  kgentopon  19774  xkotf  19821  txkgen  19888  xkococnlem  19895  imastopn  19956  kqffn  19961  opnfbas  20078  flimfnfcls  20264  alexsubALT  20286  ptcmplem1  20287  ptcmplem2  20288  ptcmplem3  20289  symgtgp  20335  tgpconcompeqg  20345  tgpconcomp  20346  ghmcnp  20348  tsmsfbas  20361  eltsms  20366  utoptop  20472  utopbas  20473  imasdsf1olem  20611  blfvalps  20621  blfps  20644  blf  20645  blcld  20743  nmoffn  20953  nmofval  20956  nmogelb  20958  nmolb  20959  nmof  20961  icccmplem1  21062  icccmplem2  21063  icccmplem3  21064  ishtpy  21207  clsocv  21425  rrxnm  21558  rrxf  21563  minveclem3b  21578  minveclem4  21582  ivthlem1  21598  ivthlem2  21599  ivthlem3  21600  ovolcl  21624  ovollb  21625  ovolgelb  21626  ovolge0  21627  ovolsslem  21630  ovolshftlem1  21655  ovolshft  21657  ovolscalem1  21659  ovolscalem2  21660  ovolsca  21661  ovolicc2lem3  21665  ovolicc2lem4  21666  ovolicc2lem5  21667  ovolicc2  21668  shftmbl  21684  iundisj  21693  dyadmax  21742  dyadmbllem  21743  dyadmbl  21744  opnmbllem  21745  iblmbf  21909  mdegmullem  22213  uc1pval  22275  mon1pval  22277  elqaalem1  22449  elqaalem3  22451  aannenlem2  22459  aalioulem2  22463  radcnvcl  22546  radcnvlt1  22547  radcnvle  22549  abelthlem4  22563  abelthlem6  22565  abelthlem9  22569  abelth  22570  atancn  22995  ftalem3  23076  ftalem4  23077  ftalem5  23078  efnnfsumcl  23104  isppw  23116  sgmval2  23145  efchtdvds  23161  sqff1o  23184  dvdsflip  23186  fsumdvdsdiaglem  23187  fsumdvdsdiag  23188  fsumdvdscom  23189  musum  23195  muinv  23197  dvdsmulf1o  23198  fsumdvdsmul  23199  sgmmul  23204  ppiub  23207  vmasum  23219  logfac2  23220  perfectlem2  23233  lgsfcl2  23305  lgsfcl  23307  lgscl  23313  lgsquadlem1  23357  lgsquadlem2  23358  rpvmasumlem  23400  rpvmasum2  23425  dchrisum0re  23426  dchrisum0lema  23427  dchrisum0lem1b  23428  dchrisum0lem1  23429  dchrisum0lem2a  23430  dchrisum0lem2  23431  dchrisum0lem3  23432  dchrisum0  23433  mudivsum  23443  mulogsum  23445  mulog2sumlem2  23448  vmalogdivsum2  23451  logsqvma  23455  logsqvma2  23456  selberglem3  23460  selberg  23461  selberg34r  23484  pntsval2  23489  pntrlog2bndlem1  23490  pntlem3  23522  tglnunirn  23663  tglnssp  23667  axcontlem2  23944  axcontlem7  23949  axcontlem8  23950  axcontlem10  23952  umgrass  23995  umgran0  23996  umisuhgra  24003  usgrass  24037  uslisushgra  24039  usgrares1  24086  usgrafilem1  24087  nbgrassvt  24109  nbgraf1olem1  24117  cusgrares  24148  hashwwlkext  24422  clwwlksswrd  24453  vdgrun  24577  vdgrfiun  24578  konigsberg  24663  frisusgranb  24673  frgrawopreg1  24727  frgrawopreg2  24728  ocsh  25877  spancl  25930  shsval2i  25981  ococin  26002  chsupid  26006  speccl  26494  atssch  26938  hatomistici  26957  chpssati  26958  iundisjf  27121  fcobijfs  27221  fpwrelmap  27228  iundisjfi  27269  esumpinfval  27719  sigagensiga  27781  measvuni  27825  imambfm  27873  dya2iocuni  27894  oms0  27906  omsmon  27907  oddpwdc  27933  eulerpartlem1  27946  eulerpartlemt  27950  eulerpartgbij  27951  eulerpartlemmf  27954  eulerpartlemgvv  27955  eulerpartlemgh  27957  eulerpartlemgs2  27959  ballotlemoex  28064  ballotlem2  28067  ballotlemfc0  28071  ballotlemfcc  28072  ballotlemfmpn  28073  ballotlemiex  28080  ballotlemsup  28083  ballotlem7  28114  ballotth  28116  lgamucov  28220  lgamucov2  28221  subfacp1lem3  28266  subfacp1lem5  28268  subfacp1lem6  28269  erdszelem2  28276  conpcon  28320  cvmliftmolem2  28367  cvmliftlem15  28383  cvmlift2lem12  28399  snmlff  28414  tfisg  28861  wfisg  28866  frinsg  28902  wlimss  28962  sltval2  28993  nodenselem4  29021  nobndlem5  29033  nofulllem5  29043  rankeq1o  29405  fin2so  29617  opnmbllem0  29627  mblfinlem1  29628  mblfinlem2  29629  ismblfin  29632  mbfposadd  29639  cnambfre  29640  finminlem  29713  fnessref  29765  finlocfin  29771  neibastop1  29780  neibastop2lem  29781  cover2  29807  indexa  29827  fdc  29841  sstotbnd2  29873  sstotbnd3  29875  igenidl  30063  prnc  30067  mzpindd  30282  fiphp3d  30357  rencldnfilem  30358  irrapx1  30368  pellexlem3  30371  pellfundre  30421  pellfundge  30422  pellfundlb  30424  pellfundglb  30425  jm2.22  30541  jm2.23  30542  rpnnen3  30578  fglmod  30623  pwssplit4  30639  pwfi2f1o  30648  hbtlem6  30682  dgraalem  30699  dgraaub  30702  itgocn  30718  rgspncl  30723  phisum  30764  lcmcllem  30802  lcmn0cl  30803  lcmledvds  30805  limcperiod  31170  sumnnodd  31172  cncfshift  31212  cncfperiod  31217  ioodvbdlimc1lem1  31261  stoweidlem14  31314  stoweidlem34  31334  stoweidlem44  31344  stoweidlem50  31350  stoweidlem51  31351  stoweidlem52  31352  stoweidlem57  31357  stoweidlem59  31359  fourierdlem19  31426  fourierdlem20  31427  fourierdlem25  31432  fourierdlem31  31438  fourierdlem37  31444  fourierdlem42  31449  fourierdlem45  31452  fourierdlem54  31461  fourierdlem64  31471  fourierdlem79  31486  bnj21  32850  bnj110  32995  bnj1204  33147  bnj1311  33159  bj-rabtr  33578  bj-rabtrAUTO  33580  bj-cmnssmnd  33724  bj-vecssmod  33731  bj-rrvecssvec  33738  toycom  33770  lkrlss  33892  atlatmstc  34116  atlatle  34117  glbconN  34173  linepsubN  34548  pmapssat  34555  pmaple  34557  pmapsub  34564  paddssat  34610  diass  35839  diaglbN  35852  diaintclN  35855  diassdvaN  35857  docaclN  35921  dibglbN  35963  dibintclN  35964  diclspsn  35991  dihglblem2N  36091  dih1dimatlem  36126  dihglb2  36139  dochval2  36149  dochcl  36150  dochvalr  36154  doch2val2  36161  dochss  36162  dochocss  36163  lclkr  36330  lclkrs  36336  lcdvbase  36390  lcdvbasess  36391  mapdunirnN  36447
  Copyright terms: Public domain W3C validator