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

Theorem ssrab2 3271
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 2565 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
2 ssab2 3270 . 2  |-  { x  |  ( x  e.  A  /\  ph ) }  C_  A
31, 2eqsstri 3221 1  |-  { x  e.  A  |  ph }  C_  A
Colors of variables: wff set class
Syntax hints:    /\ wa 358    e. wcel 1696   {cab 2282   {crab 2560    C_ wss 3165
This theorem is referenced by:  iinrab2  3981  riinrab  3993  rabexg  4180  pwnss  4192  frminex  4389  wereu2  4406  onminesb  4605  onminsb  4606  onintrab  4608  onnminsb  4611  onminex  4614  tfis  4661  omsson  4676  dmmptss  5185  ssimaex  5600  fnsuppres  5748  weniso  5868  canth  6310  riotacl  6335  riotassuni  6359  oawordeulem  6568  oeeulem  6615  nnawordex  6651  pmvalg  6799  fineqvlem  7093  ordtypelem2  7250  ordtypelem3  7251  ordtypelem4  7252  ordtypelem6  7254  hartogs  7275  wemapso2  7283  card2on  7284  wdom2d  7310  cantnfres  7395  oemapvali  7402  wemapwe  7416  tz9.12lem1  7475  tz9.12lem3  7477  rankf  7482  cplem1  7575  cardf2  7592  cardid2  7602  cardmin2  7647  acni3  7690  dfac2a  7772  kmlem1  7792  cofsmo  7911  coftr  7915  fin2i2  7960  isfin2-2  7961  enfin2i  7963  fin23lem28  7982  fin23lem30  7984  isf32lem5  7999  isf32lem6  8000  isf32lem7  8001  isf32lem8  8002  fin1a2lem9  8050  fin1a2lem11  8052  fin1a2lem12  8053  hsmexlem4  8071  hsmexlem5  8072  hsmexlem6  8073  axdc3lem4  8095  ac6num  8122  ac6  8123  zorn2lem1  8139  zorn2lem3  8141  zorn2lem4  8142  zorn2lem5  8143  ondomon  8201  alephval2  8210  pwfseqlem1  8296  pwfseqlem3  8298  wunccl  8382  tskmcl  8479  0nnq  8564  elpqn  8565  infm3  9729  infmrcl  9749  nnind  9780  uzf  10249  nnwos  10302  ublbneg  10318  supminf  10321  zsupss  10323  rpnnen1lem1  10358  rpnnen1lem2  10359  rpnnen1lem3  10360  rpnnen1lem5  10362  rpre  10376  ixxf  10682  fzf  10802  flval3  10961  expge0  11154  expge1  11155  hashbclem  11406  sqrlem3  11746  sqrlem5  11748  rlimrege0  12069  incexc2  12313  divalglem2  12610  divalglem5  12612  divalglem8  12615  bitsf  12634  bitsfzolem  12641  sadadd2lem  12666  sadadd3  12668  sadcl  12669  smupf  12685  smuval2  12689  smupvallem  12690  smucl  12691  smueqlem  12697  gcdcllem3  12708  bezoutlem2  12734  bezoutlem3  12735  maxprmfct  12808  phicl2  12852  phibnd  12855  hashdvds  12859  phiprmpw  12860  phimullem  12863  eulerthlem2  12866  eulerth  12867  odzcllem  12873  odzdvds  12876  pclem  12907  infpn2  12976  prmreclem1  12979  prmreclem2  12980  prmreclem3  12981  prmreclem4  12982  prmreclem5  12983  4sqlem13  13020  4sqlem14  13021  4sqlem17  13024  4sqlem18  13025  vdwnnlem3  13060  hashbccl  13066  ramcl2lem  13072  ramtcl  13073  ramtcl2  13074  ramtub  13075  prdsds  13379  imasdsval2  13435  mrcflem  13524  isacs1i  13575  wunnat  13846  dmcoass  13914  lubid  14132  mhmeql  14457  gsumval1  14472  nmzsubg  14674  nmznsg  14677  conjnmz  14732  conjnmzb  14733  gastacl  14779  cntzval  14813  cntzssv  14820  odlem1  14866  odcl  14867  odlem2  14870  odngen  14904  gexlem1  14906  gexcl  14907  gexlem2  14909  gexdvds  14911  sylow1lem2  14926  sylow1lem3  14927  sylow1lem4  14928  sylow1lem5  14929  pgpssslw  14941  sylow2alem2  14945  sylow2a  14946  sylow2blem3  14949  sylow3lem2  14955  oddvdssubg  15163  cyggex2  15199  ablfacrplem  15316  ablfacrp2  15318  ablfac1eu  15324  pgpfaclem1  15332  ablfaclem2  15337  ablfaclem3  15338  lssacs  15740  lspf  15747  lspsolvlem  15911  lbsextlem2  15928  lbsextlem3  15929  lbsextlem4  15930  rrgeq0  16047  rrgss  16049  asplss  16085  aspsubrg  16087  psrbagconf1o  16136  psrass1lem  16139  psrdi  16167  psrdir  16168  psrass23  16170  resspsrmul  16177  mplbas  16190  mplbasss  16193  mplsubglem  16195  mplsubrglem  16199  mplmonmul  16224  psropprmul  16332  coe1mul2lem2  16361  coe1mul2  16362  cygznlem2a  16537  ocvfval  16582  ocvval  16583  fctop  16757  cctop  16759  ppttop  16760  epttop  16762  clscld  16800  mretopd  16845  neips  16866  ordtbaslem  16934  ordtuni  16936  ordtcld1  16943  ordtcld2  16944  cnpfval  16980  iscnp2  16985  cmpcov2  17133  cmpsublem  17142  tgcmp  17144  hauscmplem  17149  concompcld  17176  1stcfb  17187  2ndc1stc  17193  2ndcdisj  17198  kgentopon  17249  xkotf  17296  txkgen  17362  xkococnlem  17369  imastopn  17427  kqffn  17432  opnfbas  17553  flimfnfcls  17739  alexsubALT  17761  ptcmplem1  17762  ptcmplem2  17763  ptcmplem3  17764  symgtgp  17800  tgpconcompeqg  17810  tgpconcomp  17811  ghmcnp  17813  tsmsfbas  17826  eltsms  17831  imasdsf1olem  17953  blfval  17963  blf  17977  blcld  18067  nmoffn  18236  nmofval  18239  nmogelb  18241  nmolb  18242  nmof  18244  icccmplem1  18343  icccmplem2  18344  icccmplem3  18345  ishtpy  18486  clsocv  18693  minveclem3b  18808  minveclem4  18812  ivthlem1  18827  ivthlem2  18828  ivthlem3  18829  ovolcl  18853  ovollb  18854  ovolgelb  18855  ovolge0  18856  ovolsslem  18859  ovolshftlem1  18884  ovolshft  18886  ovolscalem1  18888  ovolscalem2  18889  ovolsca  18890  ovolicc2lem3  18894  ovolicc2lem4  18895  ovolicc2lem5  18896  ovolicc2  18897  shftmbl  18912  iundisj  18921  dyadmax  18969  dyadmbllem  18970  dyadmbl  18971  opnmbllem  18972  iblmbf  19138  mdegmullem  19480  uc1pval  19541  mon1pval  19543  elqaalem1  19715  elqaalem3  19717  aannenlem2  19725  aalioulem2  19729  radcnvcl  19809  radcnvlt1  19810  radcnvle  19812  abelthlem4  19826  abelthlem6  19828  abelthlem9  19832  abelth  19833  atancn  20248  ftalem3  20328  ftalem4  20329  ftalem5  20330  efnnfsumcl  20356  isppw  20368  sgmval2  20397  0sgm  20398  sgmf  20399  sgmnncl  20401  efchtdvds  20413  sqff1o  20436  dvdsflip  20438  fsumdvdsdiaglem  20439  fsumdvdsdiag  20440  fsumdvdscom  20441  dvdsppwf1o  20442  musum  20447  musumsum  20448  muinv  20449  dvdsmulf1o  20450  fsumdvdsmul  20451  sgmppw  20452  sgmmul  20456  ppiub  20459  vmasum  20471  logfac2  20472  perfectlem2  20485  lgsfcl2  20557  lgsfcl  20559  lgscl  20565  lgseisenlem3  20606  lgseisenlem4  20607  lgsquadlem1  20609  lgsquadlem2  20610  rpvmasumlem  20652  dchrmusum2  20659  dchrvmasumlem1  20660  dchrvmasum2lem  20661  dchrisum0fmul  20671  dchrisum0ff  20672  dchrisum0flblem1  20673  rpvmasum2  20677  dchrisum0re  20678  dchrisum0lema  20679  dchrisum0lem1b  20680  dchrisum0lem1  20681  dchrisum0lem2a  20682  dchrisum0lem2  20683  dchrisum0lem3  20684  dchrisum0  20685  mudivsum  20695  mulogsum  20697  mulog2sumlem2  20700  vmalogdivsum2  20703  logsqvma  20707  logsqvma2  20708  selberglem3  20712  selberg  20713  selberg34r  20736  pntsval2  20741  pntrlog2bndlem1  20742  pntlem3  20774  ocsh  21878  spancl  21931  shsval2i  21982  ococin  22003  chsupid  22007  speccl  22495  atssch  22939  hatomistici  22958  chpssati  22959  ballotlemoex  23060  ballotlem2  23063  ballotlemfc0  23067  ballotlemfcc  23068  ballotlemfmpn  23069  ballotlemiex  23076  ballotlemsup  23079  ballotlemirc  23106  ballotlem7  23110  ballotth  23112  iundisjfi  23378  iundisjf  23380  esumpinfval  23456  sigagensiga  23517  measvuni  23557  imambfm  23582  subfacp1lem3  23728  subfacp1lem5  23730  subfacp1lem6  23731  erdszelem2  23738  conpcon  23781  cvmliftmolem2  23828  cvmliftlem15  23844  cvmlift2lem12  23860  umgrass  23886  umgran0  23887  vdgrf  23906  vdgrun  23908  konigsberg  23926  snmlff  23927  tfisg  24275  wfisg  24280  frinsg  24316  sltval2  24381  nodenselem4  24409  nobndlem5  24421  nofulllem5  24431  axcontlem2  24665  axcontlem7  24670  axcontlem8  24671  axcontlem10  24673  rankeq1o  24873  itgaddnclem2  25010  ump  25149  dstr  25274  prtoptop  25652  usptop  25653  finminlem  26334  fnessref  26396  finptfin  26400  finlocfin  26402  neibastop1  26411  neibastop2lem  26412  cover2  26461  indexa  26515  fdc  26558  sstotbnd2  26601  sstotbnd3  26603  igenidl  26791  prnc  26795  mzpindd  26927  fiphp3d  27005  rencldnfilem  27006  irrapx1  27016  pellexlem3  27019  pellfundre  27069  pellfundge  27070  pellfundlb  27072  pellfundglb  27073  jm2.22  27191  jm2.23  27192  rpnnen3  27228  fglmod  27274  pwssplit4  27294  dsmmbase  27304  dsmmval2  27305  dsmmsubg  27312  frlmsslsp  27351  pwfi2f1o  27363  hbtlem6  27436  dgraalem  27453  dgraaub  27456  itgocn  27472  rgspncl  27477  issubmd  27486  symgsssg  27511  symgfisg  27512  psgnghm  27540  phisum  27621  stoweidlem14  27866  stoweidlem15  27867  stoweidlem34  27886  stoweidlem44  27896  stoweidlem50  27902  stoweidlem51  27903  stoweidlem52  27904  stoweidlem57  27909  stoweidlem59  27911  usgrass  28244  nbgrassvt  28282  bnj21  29059  bnj110  29206  bnj1204  29358  bnj1311  29370  toycom  29784  lkrlss  29907  atlatmstc  30131  atlatle  30132  glbconN  30188  linepsubN  30563  pmapssat  30570  pmaple  30572  pmapsub  30579  paddssat  30625  diass  31854  diaglbN  31867  diaintclN  31870  diassdvaN  31872  docaclN  31936  dibglbN  31978  dibintclN  31979  diclspsn  32006  dihglblem2N  32106  dih1dimatlem  32141  dihglb2  32154  dochval2  32164  dochcl  32165  dochvalr  32169  doch2val2  32176  dochss  32177  dochocss  32178  lclkr  32345  lclkrs  32351  lcdvbase  32405  lcdvbasess  32406  mapdunirnN  32462
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator