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

Theorem sseqtrd 3500
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 3492 . 2  |-  ( ph  ->  ( A  C_  B  <->  A 
C_  C ) )
41, 3mpbid 213 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    C_ wss 3436
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-in 3443  df-ss 3450
This theorem is referenced by:  sseqtr4d  3501  uniintsn  4293  oeeui  7314  nnaword2  7342  oaabs2  7357  erssxp  7397  fipwuni  7949  ordtypelem7  8048  cantnflem3  8204  cdainf  8629  ficardun2  8640  ackbij1lem12  8668  ackbij1b  8676  fin1a2lem13  8849  winafp  9129  ioodisj  11769  reltrclfv  13081  prodss  14000  vdwlem11  14940  mrcssv  15519  mrcsscl  15525  mrcuni  15526  mressmrcd  15532  mreexexlem2d  15550  mreexexlem3d  15551  mreexfidimd  15555  subcss2  15747  resssetc  15986  funcsetcres2  15987  estrres  16023  poslubdg  16394  ipodrsfi  16408  acsmap2d  16424  mrelatlub  16431  mreclatBAD  16432  subsubm  16603  subsubg  16839  oppglsm  17293  subglsm  17322  lsmdisj  17330  gsumval3  17540  dprdres  17660  dprdss  17661  dprd2da  17674  dmdprdsplit2lem  17677  ablfac1b  17702  pgpfac1lem3  17709  issubdrg  18032  subsubrg  18033  islssd  18158  lspun  18209  lspssp  18210  lsslsp  18237  lsmssspx  18310  lspabs2  18342  lspabs3  18343  lspsolvlem  18364  lbsextlem3  18382  mplbas2  18693  gsumply1subr  18826  qsssubdrg  19026  obselocv  19289  lsslindf  19386  tgcl  19983  basgen  20002  tgfiss  20005  bastop1  20007  bastop2  20008  clsss2  20086  elcls3  20097  topssnei  20138  neiptopnei  20146  neitr  20194  restcls  20195  restlp  20197  ordtrest2  20218  iscncl  20283  cncls2  20287  cncls  20288  cnntr  20289  lmcls  20316  tgcmp  20414  cmpcld  20415  uncmp  20416  hauscmplem  20419  cmpfi  20421  clscon  20443  2ndcsb  20462  2ndcctbss  20468  2ndcomap  20471  nllyrest  20499  1stckgenlem  20566  kgencn2  20570  kgen2cn  20572  ptbasfi  20594  txcld  20616  txcls  20617  txbasval  20619  neitx  20620  ptcld  20626  ptclsg  20628  txnlly  20650  hausdiag  20658  txkgen  20665  xkopt  20668  xkopjcn  20669  xkococnlem  20672  cnmpt1res  20689  cnmpt2res  20690  imasnopn  20703  imasncld  20704  imasncls  20705  qtopcld  20726  qtoprest  20730  qtopcmap  20732  kqcldsat  20746  kqreglem2  20755  kqnrmlem2  20757  hmeontr  20782  neifil  20893  fgtr  20903  trnei  20905  uffixfr  20936  uffix2  20937  uffixsn  20938  elflim  20984  flimclslem  20997  fclsopn  21027  fclscmpi  21042  fclscmp  21043  alexsubALTlem3  21062  alexsubALT  21064  ptcmplem3  21067  subgntr  21119  opnsubg  21120  clssubg  21121  clsnsg  21122  cldsubg  21123  tgpconcompeqg  21124  snclseqg  21128  tsmsgsum  21151  tsmsid  21152  tgptsmscld  21163  ustssco  21227  utop2nei  21263  utop3cls  21264  utopreg  21265  cnextucn  21316  ressprdsds  21384  lpbl  21516  met2ndci  21535  prdsxmslem2  21542  metustexhalf  21569  psmetutop  21580  tgioo  21812  metdstri  21866  metdseq0  21869  metdstriOLD  21881  metdseq0OLD  21884  xlebnum  21994  clsocv  22219  metelcls  22272  cmetss  22282  relcmpcmet  22284  cmpcmet  22285  minveclem4a  22370  minveclem4aOLD  22382  uniioovol  22534  uniioombllem3  22541  limcres  22839  dvbss  22854  perfdvf  22856  dvreslem  22862  dvres2lem  22863  dvcnp2  22872  dvaddbr  22890  dvmulbr  22891  dvcmulf  22897  dvcj  22902  dvnfre  22904  dvmptres2  22914  dvmptcmul  22916  dvmptntr  22923  dvlip2  22945  dvcnvrelem2  22968  ftc1cn  22993  taylfvallem1  23310  taylply2  23321  taylply  23322  dvtaylp  23323  dvntaylp  23324  dvntaylp0  23325  taylthlem1  23326  taylthlem2  23327  ulmdvlem3  23355  pserulm  23375  shsub2  26976  spanssoc  27000  shub2  27034  ococin  27059  ssjo  27098  chub2  27159  spanpr  27231  elnlfn  27579  mdslj1i  27970  mdslmd3i  27983  mdexchi  27986  chirredlem1  28041  atcvat3i  28047  mdsymlem1  28054  mdsymlem5  28058  imadifxp  28214  qtophaus  28671  locfinreflem  28675  fsumcvg4  28764  esum2d  28922  omsmon  29134  omssubadd  29136  omsmonOLD  29138  omssubaddOLD  29140  carsggect  29158  carsgclctun  29161  sitgclg  29183  eulerpartlemgf  29220  cvmscld  30004  cvmliftmolem1  30012  cvmlift2lem9  30042  cvmlift2lem11  30044  cvmlift3lem6  30055  nodense  30583  opnregcld  30991  ivthALT  30996  neibastop2  31022  fnemeet1  31027  fnejoin1  31029  poimirlem11  31915  poimirlem12  31916  poimirlem30  31934  ftc1cnnc  31980  sstotbnd  32071  ssbnd  32084  heibor1lem  32105  heiborlem3  32109  heibor  32117  lsmsat  32543  lssats  32547  lcvexchlem3  32571  lsatcvat3  32587  lkrscss  32633  lkrpssN  32698  pmod1i  33382  pclbtwnN  33431  pclunN  33432  pclss2polN  33455  pcl0N  33456  sspmaplubN  33459  paddunN  33461  pnonsingN  33467  pclfinclN  33484  osumcllem4N  33493  dia2dimlem13  34613  dvhopellsm  34654  dvadiaN  34665  dicelval1stN  34725  dicelval2nd  34726  dihssxp  34789  dihvalrel  34816  dochsscl  34905  dihoml4  34914  dochnoncon  34928  dvh3dim3N  34986  lcfrlem2  35080  lcfrlem5  35083  lcfr  35122  lcdlsp  35158  mapdsn  35178  mapdlsm  35201  mapdpglem1  35209  mapdindp0  35256  hlhilocv  35497  rntrclfvOAI  35502  ismrcd1  35509  ismrcd2  35510  coeq0i  35564  hbtlem6  35958  rgspnval  36004  iocinico  36066  trclubNEW  36196  wessf1ornlem  37420  iccdifprioo  37566  cncfuni  37704  cncfiooicclem1  37711  dvresntr  37728  dvmptresicc  37731  itgsubsticclem  37792  fourierdlem42  37952  fourierdlem42OLD  37953  fourierdlem48  37958  fourierdlem49  37959  fourierdlem50  37960  prsal  38100  intsaluni  38109  sge0f1o  38132  sge0split  38159  ismeannd  38213  caragensspw  38238  caragendifcl  38243  carageniuncl  38252  caratheodorylem1  38255  hoicvrrex  38282  ovnssle  38287  ovn02  38294  ovnsubadd  38298  hoidmv1le  38320  subsubmgm  39417
  Copyright terms: Public domain W3C validator