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

Theorem sseqtrd 3216
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 3208 . 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 1625    C_ wss 3154
This theorem is referenced by:  sseqtr4d  3217  uniintsn  3901  oeeui  6602  nnaword2  6630  oaabs2  6645  erssxp  6685  fipwuni  7181  ordtypelem7  7241  cantnflem3  7395  cdainf  7820  ficardun2  7831  ackbij1lem12  7859  ackbij1b  7867  fin1a2lem13  8040  winafp  8321  ioodisj  10767  vdwlem11  13040  mrcssv  13518  mrcsscl  13524  mrcuni  13525  mressmrcd  13531  mreexexlem2d  13549  mreexexlem3d  13550  mreexfidimd  13554  subcss2  13719  resssetc  13926  funcsetcres2  13927  poslubdg  14254  ipodrsfi  14268  acsmap2d  14284  mrelatlub  14291  mreclat  14292  subsubm  14436  subsubg  14642  oppglsm  14955  subglsm  14984  lsmdisj  14992  gsumval3  15193  dprdres  15265  dprdss  15266  dprd2da  15279  dmdprdsplit2lem  15282  ablfac1b  15307  pgpfac1lem3  15314  issubdrg  15572  subsubrg  15573  islssd  15695  lspun  15746  lspssp  15747  lsslsp  15774  lsmssspx  15843  lspabs2  15875  lspabs3  15876  lspsolvlem  15897  lbsextlem3  15915  mplbas2  16214  qsssubdrg  16433  obselocv  16630  tgcl  16709  basgen  16728  tgfiss  16731  bastop1  16733  bastop2  16734  clsss2  16811  elcls3  16822  topssnei  16863  restcls  16913  restlp  16915  ordtrest2  16936  iscncl  17000  cncls2  17004  cncls  17005  cnntr  17006  lmcls  17032  tgcmp  17130  cmpcld  17131  uncmp  17132  hauscmplem  17135  cmpfi  17137  clscon  17158  2ndcsb  17177  2ndcctbss  17183  2ndcomap  17186  nllyrest  17214  1stckgenlem  17250  kgencn2  17254  kgen2cn  17256  ptbasfi  17278  txcld  17300  txcls  17301  txbasval  17303  ptcld  17309  ptclsg  17311  txnlly  17333  hausdiag  17341  txkgen  17348  xkopt  17351  xkopjcn  17352  xkococnlem  17355  cnmpt1res  17372  cnmpt2res  17373  qtopcld  17406  qtoprest  17410  qtopcmap  17412  kqcldsat  17426  kqreglem2  17435  kqnrmlem2  17437  hmeontr  17462  neifil  17577  fgtr  17587  trnei  17589  uffixfr  17620  uffix2  17621  uffixsn  17622  elflim  17668  flimclslem  17681  fclsopn  17711  fclscmpi  17726  fclscmp  17727  alexsubALTlem3  17745  alexsubALT  17747  ptcmplem3  17750  subgntr  17791  opnsubg  17792  clssubg  17793  clsnsg  17794  cldsubg  17795  tgpconcompeqg  17796  snclseqg  17800  tsmsgsum  17823  tsmsid  17824  tgptsmscld  17835  ressprdsds  17937  lpbl  18051  met2ndci  18070  prdsxmslem2  18077  tgioo  18304  metdstri  18357  metdseq0  18360  xlebnum  18465  clsocv  18679  metelcls  18732  cmetss  18742  relcmpcmet  18744  cmpcmet  18745  minveclem4a  18796  uniioovol  18936  uniioombllem3  18942  limcres  19238  dvbss  19253  perfdvf  19255  dvreslem  19261  dvres2lem  19262  dvcnp2  19271  dvaddbr  19289  dvmulbr  19290  dvcmulf  19296  dvcj  19301  dvnfre  19303  dvmptres2  19313  dvmptcmul  19315  dvmptntr  19322  dvlip2  19344  dvcnvrelem2  19367  ftc1cn  19392  taylfvallem1  19738  taylply2  19749  taylply  19750  dvtaylp  19751  dvntaylp  19752  dvntaylp0  19753  taylthlem1  19754  taylthlem2  19755  ulmdvlem3  19781  pserulm  19800  shsub2  21906  spanssoc  21930  shub2  21964  ococin  21989  ssjo  22028  chub2  22089  spanpr  22161  elnlfn  22510  mdslj1i  22901  mdslmd3i  22914  mdexchi  22917  chirredlem1  22972  atcvat3i  22978  mdsymlem1  22985  mdsymlem5  22989  esumpfinvallem  23444  cvmscld  23806  cvmliftmolem1  23814  cvmlift2lem9  23844  cvmlift2lem11  23846  cvmlift3lem6  23857  nodense  24345  prdnei  25584  dualalg  25793  opnregcld  26259  ivthALT  26269  neibastop2  26321  fnemeet1  26326  fnejoin1  26328  sstotbnd  26510  ssbnd  26523  heibor1lem  26544  heiborlem3  26548  heibor  26556  ismrcd1  26784  ismrcd2  26785  coeq0i  26843  lsslindf  27311  hbtlem6  27344  rgspnval  27384  stoweidlem34  27794  lsmsat  29271  lssats  29275  lcvexchlem3  29299  lsatcvat3  29315  lkrscss  29361  lkrpssN  29426  pmod1i  30110  pclbtwnN  30159  pclunN  30160  pclss2polN  30183  pcl0N  30184  sspmaplubN  30187  paddunN  30189  pnonsingN  30195  pclfinclN  30212  osumcllem4N  30221  dia2dimlem13  31339  dvhopellsm  31380  dvadiaN  31391  dicelval1stN  31451  dicelval2nd  31452  dihssxp  31515  dihvalrel  31542  dochsscl  31631  dihoml4  31640  dochnoncon  31654  dvh3dim3N  31712  lcfrlem2  31806  lcfrlem5  31809  lcfr  31848  lcdlsp  31884  mapdsn  31904  mapdlsm  31927  mapdpglem1  31935  mapdindp0  31982  hlhilocv  32223
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-in 3161  df-ss 3168
  Copyright terms: Public domain W3C validator