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

Theorem ssrab2 3571
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 2813 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
2 ssab2 3570 . 2  |-  { x  |  ( x  e.  A  /\  ph ) }  C_  A
31, 2eqsstri 3519 1  |-  { x  e.  A  |  ph }  C_  A
Colors of variables: wff setvar class
Syntax hints:    /\ wa 367    e. wcel 1823   {cab 2439   {crab 2808    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2813  df-in 3468  df-ss 3475
This theorem is referenced by:  ssrabeq  3572  iinrab2  4378  riinrab  4391  rabexg  4587  pwnss  4602  frminex  4848  wereu2  4865  dmmptss  5486  ssimaex  5913  f1oresrab  6039  fnsuppresOLD  6107  weniso  6225  canth  6229  riotacl  6246  riotassuniOLD  6268  onminesb  6606  onminsb  6607  onintrab  6609  onnminsb  6612  onminex  6615  tfis  6662  omsson  6677  suppssdm  6904  fnsuppres  6919  oawordeulem  7195  oeeulem  7242  nnawordex  7278  pmvalg  7423  fineqvlem  7727  ordtypelem2  7936  ordtypelem3  7937  ordtypelem4  7938  ordtypelem6  7940  hartogs  7961  wemapso2OLD  7969  wemapso2lem  7970  card2on  7972  wdom2d  7998  oemapvali  8094  wemapwe  8130  wemapweOLD  8131  tz9.12lem1  8196  tz9.12lem3  8198  rankf  8203  cplem1  8298  cardf2  8315  cardid2  8325  cardmin2  8370  acni3  8419  dfac2a  8501  cofsmo  8640  coftr  8644  fin2i2  8689  isfin2-2  8690  enfin2i  8692  fin23lem28  8711  fin23lem30  8713  isf32lem5  8728  isf32lem6  8729  isf32lem7  8730  isf32lem8  8731  fin1a2lem11  8781  fin1a2lem12  8782  hsmexlem4  8800  hsmexlem5  8801  hsmexlem6  8802  axdc3lem4  8824  ac6num  8850  ac6  8851  zorn2lem1  8867  zorn2lem3  8869  zorn2lem4  8870  zorn2lem5  8871  ondomon  8929  alephval2  8938  pwfseqlem1  9025  pwfseqlem3  9027  wunccl  9111  tskmcl  9208  0nnq  9291  elpqn  9292  infm3  10497  infmrcl  10517  uzf  11085  nnwos  11150  supminf  11170  zsupss  11172  rpnnen1lem1  11209  rpnnen1lem2  11210  rpnnen1lem3  11211  rpnnen1lem5  11213  rpre  11227  ixxf  11542  fzf  11679  flval3  11932  rabssnn0fi  12077  expge0  12184  expge1  12185  hashbclem  12485  sqrlem3  13160  sqrlem5  13162  rlimrege0  13484  incexc2  13732  divalglem2  14137  divalglem5  14139  divalglem8  14142  bitsf  14161  bitsfzolem  14168  sadadd2lem  14193  sadadd3  14195  sadcl  14196  smupf  14212  smuval2  14216  smupvallem  14217  smucl  14218  smueqlem  14224  gcdcllem3  14235  bezoutlem2  14261  bezoutlem3  14262  maxprmfct  14338  phicl2  14382  phibnd  14385  hashdvds  14389  phiprmpw  14390  phimullem  14393  eulerthlem2  14396  eulerth  14397  odzcllem  14403  odzdvds  14406  pclem  14446  infpn2  14515  prmreclem1  14518  prmreclem2  14519  prmreclem3  14520  prmreclem4  14521  prmreclem5  14522  4sqlem13  14559  4sqlem14  14560  4sqlem17  14563  4sqlem18  14564  vdwnnlem3  14599  hashbccl  14605  ramcl2lem  14611  ramtcl  14612  ramtcl2  14613  ramtub  14614  prdsds  14953  imasdsval2  15005  mrcflem  15095  isacs1i  15146  wunnat  15444  dmcoass  15544  lublecl  15818  lubid  15819  gsumval1  16103  issubmd  16179  mhmeql  16194  nmzsubg  16441  nmznsg  16444  conjnmz  16499  conjnmzb  16500  gastacl  16546  cntzval  16558  cntzssv  16565  symgsssg  16691  symgfisg  16692  pmtrdifellem4  16703  odlem1  16758  odlem2  16762  odngen  16796  gexlem1  16798  gexlem2  16801  sylow1lem2  16818  sylow1lem3  16819  sylow1lem4  16820  sylow1lem5  16821  sylow2alem2  16837  sylow2a  16838  sylow2blem3  16841  sylow3lem2  16847  oddvdssubg  17060  cyggex2  17098  ablfacrplem  17311  ablfacrp2  17313  ablfac1eu  17319  pgpfaclem1  17327  ablfaclem2  17332  ablfaclem3  17333  lssacs  17808  lspf  17815  lspsolvlem  17983  lbsextlem2  18000  lbsextlem3  18001  lbsextlem4  18002  rrgeq0  18133  rrgss  18136  asplss  18173  aspsubrg  18175  psrbagconf1o  18221  psrass1lem  18224  psrdi  18256  psrdir  18257  psrass23l  18258  psrass23  18260  resspsrmul  18267  mplbas  18281  mplbasOLD  18283  mplbasss  18286  mplsubglem  18288  mplsubglemOLD  18290  mplsubrglem  18295  mplsubrglemOLD  18296  mplmonmul  18321  psropprmul  18474  coe1mul2lem2  18504  cygznlem2a  18779  psgnghm  18789  ocvfval  18870  ocvval  18871  dsmmbase  18939  dsmmval2  18940  dsmmsubg  18947  frlmsslsp  18998  scmatlss  19194  smadiadet  19339  pmatcoe1fsupp  19369  cpmatsubgpmat  19388  fctop  19672  cctop  19674  ppttop  19675  epttop  19677  clscld  19715  mretopd  19760  neips  19781  neiptopnei  19800  ordtbaslem  19856  ordtuni  19858  ordtcld1  19865  ordtcld2  19866  cnpfval  19902  iscnp2  19907  cmpcov2  20057  cmpsublem  20066  tgcmp  20068  hauscmplem  20073  concompcld  20101  1stcfb  20112  2ndc1stc  20118  2ndcdisj  20123  finlocfin  20187  kgentopon  20205  xkotf  20252  txkgen  20319  xkococnlem  20326  imastopn  20387  kqffn  20392  opnfbas  20509  flimfnfcls  20695  alexsubALT  20717  ptcmplem1  20718  ptcmplem2  20719  ptcmplem3  20720  symgtgp  20766  tgpconcompeqg  20776  tgpconcomp  20777  ghmcnp  20779  tsmsfbas  20792  eltsms  20797  utoptop  20903  utopbas  20904  imasdsf1olem  21042  blfvalps  21052  blfps  21075  blf  21076  blcld  21174  nmoffn  21384  nmofval  21387  nmogelb  21389  nmolb  21390  nmof  21392  icccmplem1  21493  icccmplem2  21494  icccmplem3  21495  ishtpy  21638  clsocv  21856  rrxnm  21989  rrxf  21994  minveclem3b  22009  minveclem4  22013  ivthlem1  22029  ivthlem2  22030  ivthlem3  22031  ovolcl  22055  ovollb  22056  ovolgelb  22057  ovolge0  22058  ovolsslem  22061  ovolshftlem1  22086  ovolshft  22088  ovolscalem1  22090  ovolscalem2  22091  ovolsca  22092  ovolicc2lem3  22096  ovolicc2lem4  22097  ovolicc2lem5  22098  ovolicc2  22099  shftmbl  22115  iundisj  22124  dyadmax  22173  dyadmbllem  22174  dyadmbl  22175  opnmbllem  22176  iblmbf  22340  mdegmullem  22644  uc1pval  22706  mon1pval  22708  elqaalem1  22881  elqaalem3  22883  aannenlem2  22891  aalioulem2  22895  radcnvcl  22978  radcnvlt1  22979  radcnvle  22981  abelthlem4  22995  abelthlem6  22997  abelthlem9  23001  abelth  23002  atancn  23464  ftalem3  23546  ftalem4  23547  ftalem5  23548  efnnfsumcl  23574  isppw  23586  sgmval2  23615  efchtdvds  23631  sqff1o  23654  dvdsflip  23656  fsumdvdsdiaglem  23657  fsumdvdsdiag  23658  fsumdvdscom  23659  musum  23665  muinv  23667  dvdsmulf1o  23668  fsumdvdsmul  23669  sgmmul  23674  ppiub  23677  vmasum  23689  logfac2  23690  perfectlem2  23703  lgsfcl2  23775  lgsfcl  23777  lgscl  23783  lgsquadlem1  23827  lgsquadlem2  23828  rpvmasumlem  23870  rpvmasum2  23895  dchrisum0re  23896  dchrisum0lema  23897  dchrisum0lem1b  23898  dchrisum0lem1  23899  dchrisum0lem2a  23900  dchrisum0lem2  23901  dchrisum0lem3  23902  dchrisum0  23903  mudivsum  23913  mulogsum  23915  mulog2sumlem2  23918  vmalogdivsum2  23921  logsqvma  23925  logsqvma2  23926  selberglem3  23930  selberg  23931  selberg34r  23954  pntsval2  23959  pntrlog2bndlem1  23960  pntlem3  23992  tglnunirn  24136  tglnssp  24140  axcontlem2  24470  axcontlem7  24475  axcontlem8  24476  axcontlem10  24478  umgrass  24521  umgran0  24522  umisuhgra  24529  usgrass  24563  uslisushgra  24565  usgrares1  24612  usgrafilem1  24613  nbgrassvt  24635  nbgraf1olem1  24643  cusgrares  24674  hashwwlkext  24948  clwwlksswrd  24979  vdgrun  25103  vdgrfiun  25104  konigsberg  25189  frisusgranb  25199  frgrawopreg1  25252  frgrawopreg2  25253  ocsh  26399  spancl  26452  shsval2i  26503  ococin  26524  chsupid  26528  speccl  27016  atssch  27460  hatomistici  27479  chpssati  27480  iundisjf  27659  aciunf1  27730  fcobijfs  27780  fpwrelmap  27787  iundisjfi  27835  locfinreflem  28078  esumrnmpt2  28297  esumpinfval  28302  sigagensiga  28371  measvuni  28422  imambfm  28470  dya2iocuni  28491  omscl  28503  oms0  28505  omsmon  28506  omssubadd  28508  carsgcl  28512  oddpwdc  28557  eulerpartlem1  28570  eulerpartlemt  28574  eulerpartgbij  28575  eulerpartlemmf  28578  eulerpartlemgvv  28579  eulerpartlemgh  28581  eulerpartlemgs2  28583  ballotlem2  28691  ballotlemfc0  28695  ballotlemfcc  28696  ballotlemfmpn  28697  ballotlemiex  28704  ballotlemsup  28707  ballotlem7  28738  ballotth  28740  lgamucov  28844  lgamucov2  28845  subfacp1lem3  28890  subfacp1lem5  28892  subfacp1lem6  28893  erdszelem2  28900  conpcon  28944  cvmliftmolem2  28991  cvmliftlem15  29007  cvmlift2lem12  29023  snmlff  29038  tfisg  29524  wfisg  29529  frinsg  29565  wlimss  29625  sltval2  29656  nodenselem4  29684  nobndlem5  29696  nofulllem5  29706  rankeq1o  30056  fin2so  30280  opnmbllem0  30290  mblfinlem1  30291  mblfinlem2  30292  ismblfin  30295  mbfposadd  30302  cnambfre  30303  finminlem  30376  fnessref  30415  neibastop1  30417  neibastop2lem  30418  cover2  30444  indexa  30464  fdc  30478  sstotbnd2  30510  sstotbnd3  30512  igenidl  30700  prnc  30704  mzpindd  30918  fiphp3d  30992  rencldnfilem  30993  irrapx1  31003  pellexlem3  31006  pellfundre  31056  pellfundge  31057  pellfundlb  31059  pellfundglb  31060  jm2.22  31176  jm2.23  31177  rpnnen3  31213  fglmod  31258  pwssplit4  31274  pwfi2f1o  31283  pwfi2f1oOLD  31284  hbtlem6  31319  dgraalem  31335  dgraaub  31338  itgocn  31354  rgspncl  31359  phisum  31400  lcmcllem  31443  lcmn0cl  31444  lcmledvds  31446  binomcxplemdvbinom  31499  binomcxplemcvg  31500  binomcxplemnotnn0  31502  limcperiod  31873  sumnnodd  31875  cncfshift  31915  cncfperiod  31920  ioodvbdlimc1lem1  31967  dvnprodlem1  31982  dvnprodlem2  31983  stoweidlem14  32035  stoweidlem34  32055  stoweidlem44  32065  stoweidlem50  32071  stoweidlem51  32072  stoweidlem52  32073  stoweidlem57  32078  stoweidlem59  32080  fourierdlem19  32147  fourierdlem20  32148  fourierdlem25  32153  fourierdlem31  32159  fourierdlem37  32165  fourierdlem42  32170  fourierdlem51  32179  fourierdlem54  32182  fourierdlem64  32192  fourierdlem79  32207  elaa2lem  32255  etransclem16  32272  etransclem24  32280  etransclem31  32287  etransclem33  32289  etransclem34  32290  etransclem48  32304  rabsubmgmd  32851  mgmhmeql  32863  oddibas  32873  2zlidl  32994  2zrngbas  32996  2zrng0  32998  bnj21  34171  bnj110  34317  bnj1204  34469  bnj1311  34481  bj-rabtr  34898  bj-rabtrAUTO  34900  bj-cmnssmnd  35052  bj-vecssmod  35059  bj-rrvecssvec  35066  toycom  35095  lkrlss  35217  atlatmstc  35441  atlatle  35442  glbconN  35498  linepsubN  35873  pmapssat  35880  pmaple  35882  pmapsub  35889  paddssat  35935  diass  37166  diaglbN  37179  diaintclN  37182  diassdvaN  37184  docaclN  37248  dibglbN  37290  dibintclN  37291  diclspsn  37318  dihglblem2N  37418  dih1dimatlem  37453  dihglb2  37466  dochval2  37476  dochcl  37477  dochvalr  37481  doch2val2  37488  dochss  37489  dochocss  37490  lclkr  37657  lclkrs  37663  lcdvbase  37717  lcdvbasess  37718  mapdunirnN  37774
  Copyright terms: Public domain W3C validator