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

Theorem sseqtrd 3214
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)
Hypotheses
Ref Expression
sseqtrd.1  |-  ( ph  ->  A  C_  B )
sseqtrd.2  |-  ( ph  ->  B  =  C )
Assertion
Ref Expression
sseqtrd  |-  ( ph  ->  A  C_  C )

Proof of Theorem sseqtrd
StepHypRef Expression
1 sseqtrd.1 . 2  |-  ( ph  ->  A  C_  B )
2 sseqtrd.2 . . 3  |-  ( ph  ->  B  =  C )
32sseq2d 3206 . 2  |-  ( ph  ->  ( A  C_  B  <->  A 
C_  C ) )
41, 3mpbid 201 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    C_ wss 3152
This theorem is referenced by:  sseqtr4d  3215  uniintsn  3899  oeeui  6600  nnaword2  6628  oaabs2  6643  erssxp  6683  fipwuni  7179  ordtypelem7  7239  cantnflem3  7393  cdainf  7818  ficardun2  7829  ackbij1lem12  7857  ackbij1b  7865  fin1a2lem13  8038  winafp  8319  ioodisj  10765  vdwlem11  13038  mrcssv  13516  mrcsscl  13522  mrcuni  13523  mressmrcd  13529  mreexexlem2d  13547  mreexexlem3d  13548  mreexfidimd  13552  subcss2  13717  resssetc  13924  funcsetcres2  13925  poslubdg  14252  ipodrsfi  14266  acsmap2d  14282  mrelatlub  14289  mreclat  14290  subsubm  14434  subsubg  14640  oppglsm  14953  subglsm  14982  lsmdisj  14990  gsumval3  15191  dprdres  15263  dprdss  15264  dprd2da  15277  dmdprdsplit2lem  15280  ablfac1b  15305  pgpfac1lem3  15312  issubdrg  15570  subsubrg  15571  islssd  15693  lspun  15744  lspssp  15745  lsslsp  15772  lsmssspx  15841  lspabs2  15873  lspabs3  15874  lspsolvlem  15895  lbsextlem3  15913  mplbas2  16212  qsssubdrg  16431  obselocv  16628  tgcl  16707  basgen  16726  tgfiss  16729  bastop1  16731  bastop2  16732  clsss2  16809  elcls3  16820  topssnei  16861  restcls  16911  restlp  16913  ordtrest2  16934  iscncl  16998  cncls2  17002  cncls  17003  cnntr  17004  lmcls  17030  tgcmp  17128  cmpcld  17129  uncmp  17130  hauscmplem  17133  cmpfi  17135  clscon  17156  2ndcsb  17175  2ndcctbss  17181  2ndcomap  17184  nllyrest  17212  1stckgenlem  17248  kgencn2  17252  kgen2cn  17254  ptbasfi  17276  txcld  17298  txcls  17299  txbasval  17301  ptcld  17307  ptclsg  17309  txnlly  17331  hausdiag  17339  txkgen  17346  xkopt  17349  xkopjcn  17350  xkococnlem  17353  cnmpt1res  17370  cnmpt2res  17371  qtopcld  17404  qtoprest  17408  qtopcmap  17410  kqcldsat  17424  kqreglem2  17433  kqnrmlem2  17435  hmeontr  17460  neifil  17575  fgtr  17585  trnei  17587  uffixfr  17618  uffix2  17619  uffixsn  17620  elflim  17666  flimclslem  17679  fclsopn  17709  fclscmpi  17724  fclscmp  17725  alexsubALTlem3  17743  alexsubALT  17745  ptcmplem3  17748  subgntr  17789  opnsubg  17790  clssubg  17791  clsnsg  17792  cldsubg  17793  tgpconcompeqg  17794  snclseqg  17798  tsmsgsum  17821  tsmsid  17822  tgptsmscld  17833  ressprdsds  17935  lpbl  18049  met2ndci  18068  prdsxmslem2  18075  tgioo  18302  metdstri  18355  metdseq0  18358  xlebnum  18463  clsocv  18677  metelcls  18730  cmetss  18740  relcmpcmet  18742  cmpcmet  18743  minveclem4a  18794  uniioovol  18934  uniioombllem3  18940  limcres  19236  dvbss  19251  perfdvf  19253  dvreslem  19259  dvres2lem  19260  dvcnp2  19269  dvaddbr  19287  dvmulbr  19288  dvcmulf  19294  dvcj  19299  dvnfre  19301  dvmptres2  19311  dvmptcmul  19313  dvmptntr  19320  dvlip2  19342  dvcnvrelem2  19365  ftc1cn  19390  taylfvallem1  19736  taylply2  19747  taylply  19748  dvtaylp  19749  dvntaylp  19750  dvntaylp0  19751  taylthlem1  19752  taylthlem2  19753  ulmdvlem3  19779  pserulm  19798  shsub2  21904  spanssoc  21928  shub2  21962  ococin  21987  ssjo  22026  chub2  22087  spanpr  22159  elnlfn  22508  mdslj1i  22899  mdslmd3i  22912  mdexchi  22915  chirredlem1  22970  atcvat3i  22976  mdsymlem1  22983  mdsymlem5  22987  esumpfinvallem  23442  cvmscld  23804  cvmliftmolem1  23812  cvmlift2lem9  23842  cvmlift2lem11  23844  cvmlift3lem6  23855  nodense  24343  prdnei  25573  dualalg  25782  opnregcld  26248  ivthALT  26258  neibastop2  26310  fnemeet1  26315  fnejoin1  26317  sstotbnd  26499  ssbnd  26512  heibor1lem  26533  heiborlem3  26537  heibor  26545  ismrcd1  26773  ismrcd2  26774  coeq0i  26832  lsslindf  27300  hbtlem6  27333  rgspnval  27373  stoweidlem34  27783  lsmsat  29198  lssats  29202  lcvexchlem3  29226  lsatcvat3  29242  lkrscss  29288  lkrpssN  29353  pmod1i  30037  pclbtwnN  30086  pclunN  30087  pclss2polN  30110  pcl0N  30111  sspmaplubN  30114  paddunN  30116  pnonsingN  30122  pclfinclN  30139  osumcllem4N  30148  dia2dimlem13  31266  dvhopellsm  31307  dvadiaN  31318  dicelval1stN  31378  dicelval2nd  31379  dihssxp  31442  dihvalrel  31469  dochsscl  31558  dihoml4  31567  dochnoncon  31581  dvh3dim3N  31639  lcfrlem2  31733  lcfrlem5  31736  lcfr  31775  lcdlsp  31811  mapdsn  31831  mapdlsm  31854  mapdpglem1  31862  mapdindp0  31909  hlhilocv  32150
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-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator