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

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

Proof of Theorem sseqtr4d
StepHypRef Expression
1 sseqtr4d.1 . 2  |-  ( ph  ->  A  C_  B )
2 sseqtr4d.2 . . 3  |-  ( ph  ->  C  =  B )
32eqcomd 2462 . 2  |-  ( ph  ->  B  =  C )
41, 3sseqtrd 3525 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1398    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-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3468  df-ss 3475
This theorem is referenced by:  syl5sseqr  3538  reusv6OLD  4648  fnfvima  6125  oaordi  7187  omordi  7207  omlimcl  7219  oen0  7227  domunsncan  7610  f1opwfi  7816  cantnfle  8081  cantnflt  8082  cantnflem1d  8098  cantnfleOLD  8111  cantnfltOLD  8112  cantnflem1dOLD  8121  r1pwss  8193  rankxplim3  8290  acndom2  8426  fodomfi2  8432  cflm  8621  cflim2  8634  isf34lem5  8749  isf34lem7  8750  isf34lem6  8751  axdc2lem  8819  ttukeylem5  8884  wunex2  9105  ccatass  12597  swrdval2  12639  swrdccatin12  12710  splfv2a  12726  revccat  12734  rtrclreclem1  12976  rtrclreclem2  12977  sumrblem  13618  prodrblem  13821  dfphi2  14391  vdwlem1  14586  imasaddfnlem  15020  imasaddvallem  15021  imasvscafn  15029  imasvscaval  15030  mreexexlem4d  15139  mreexfidimd  15142  sscpwex  15306  acsmap2d  16011  gsumress  16105  subsubm  16190  frmdsssubm  16231  frmdss2  16233  subsubg  16426  cntzmhm2  16579  cntzcmnf  17053  ablcntzd  17065  gsumzsubmcl  17130  gsumzsubmclOLD  17131  gsumconst  17155  gsumzmhm  17158  gsumzmhmOLD  17159  gsumzoppg  17168  subgdmdprd  17279  dprdcntz2  17284  dprd2da  17289  dmdprdsplit2lem  17292  ablfac1eu  17322  pgpfaclem1  17330  pgpfaclem2  17331  issubdrg  17652  subsubrg  17653  lmhmlsp  17893  lspsntri  17941  lspindpi  17976  lidldvgen  18101  opsrtoslem2  18347  gsumfsum  18682  mrccss  18901  frlmsslsp  19001  scmatsgrp1  19194  toponss  19600  ssntr  19729  elcls3  19754  toponmre  19764  neiptoptop  19802  neiptopnei  19803  neitr  19851  ordtbas  19863  ordtopn1  19865  ordtopn2  19866  iscnp3  19915  tgcn  19923  tgcnp  19924  ssidcn  19926  cnclsi  19943  cncls  19945  cncnp  19951  lmcld  19974  tgcmp  20071  cnconn  20092  conima  20095  clscon  20100  concompcld  20104  1stccnp  20132  kgentopon  20208  llycmpkgen2  20220  1stckgen  20224  kgencn2  20227  ptopn  20253  txcls  20274  ptpjcn  20281  ptclsg  20285  xkoccn  20289  txcnp  20290  ptcnplem  20291  txcmplem2  20312  xkoptsub  20324  xkopt  20325  xkoco2cn  20328  xkococnlem  20329  xkoinjcn  20357  imasnopn  20360  imasncld  20361  imasncls  20362  qtopkgen  20380  basqtop  20381  tgqtop  20382  qtoprest  20387  kqsat  20401  kqcldsat  20403  kqnrmlem1  20413  kqnrmlem2  20414  hmeontr  20439  reghmph  20463  nrmhmph  20464  fmfnfmlem4  20627  fmfnfm  20628  flimopn  20645  flimclslem  20654  flfnei  20661  lmflf  20675  txflf  20676  fclsopn  20684  fclsfnflim  20697  alexsublem  20713  ptcmplem3  20723  cnextcn  20736  symgtgp  20769  submtmd  20772  subgtgp  20773  clssubg  20776  clsnsg  20777  tgpconcompeqg  20779  snclseqg  20783  tsmscls  20805  trust  20901  restutop  20909  restutopopn  20910  utop3cls  20923  utopreg  20924  trcfilu  20966  blssec  21107  prdsbl  21163  blssopn  21167  metcnp  21213  cfilucfilOLD  21241  cfilucfil  21242  metutopOLD  21254  psmetutop  21255  iccntr  21495  icccmplem2  21497  reconnlem1  21500  metnrmlem1a  21531  metnrmlem1  21532  metnrmlem2  21533  metnrmlem3  21534  cnheibor  21624  lebnumlem1  21630  lebnumlem3  21632  lebnumii  21635  clsocv  21859  iscfil2  21874  iscmet3  21901  cmetss  21922  relcmpcmet  21924  bcthlem5  21936  itg1addlem5  22276  perfdvf  22476  dvres3  22486  dvres3a  22487  dvcmul  22516  dvcmulf  22517  dvlip2  22565  lhop1lem  22583  dvcnvrelem1  22587  dvcnvrelem2  22588  dvcnvre  22589  dvcvx  22590  plyco0  22758  plyaddlem1  22779  plymullem1  22780  aalioulem3  22899  ulmdvlem1  22964  axcontlem10  24481  eengtrkg  24493  eupares  25180  ghsubgolemOLD  25573  hsupunss  26462  pjpjpre  26538  ssmd2  27432  superpos  27474  atexch  27501  curry2ima  27758  ordtconlem1  28144  measiuns  28428  imambfm  28473  cnmbfm  28474  dya2iocnrect  28492  omsfval  28505  omssubaddlem  28510  omssubadd  28511  totprobd  28632  fzssfzo  28757  signstfvn  28793  cvmsss2  28986  cvmliftmolem1  28993  cvmliftlem3  28999  cvmlift2lem9  29023  cvmlift2lem11  29025  cvmlift3lem6  29036  cvmlift3lem7  29037  ssmclslem  29192  mclsax  29196  mclsppslem  29210  mclspps  29211  dfrdg2  29471  trpredtr  29556  itg2addnclem2  30310  neiin  30393  neibastop2  30422  filnetlem4  30442  cnres2  30502  sstotbnd2  30513  sstotbnd  30514  prdstotbnd  30533  heibor1lem  30548  igenval2  30706  fnwe2lem2  31239  lnmlsslnm  31269  lmhmfgima  31272  hbtlem6  31322  dvsconst  31479  dvsinax  31950  dvbdfbdioolem1  31967  itgsinexplem1  31994  itgperiod  32022  stoweidlem39  32063  dirkeritg  32126  fourierdlem48  32179  fourierdlem49  32180  fourierdlem70  32201  fourierdlem71  32202  fourierdlem81  32212  pfxccatin12  32672  subsubmgm  32876  rmsuppss  33236  bnj999  34435  bnj1408  34512  bnj1442  34525  bnj1450  34526  bnj1501  34543  lshpnelb  35125  lcvexchlem4  35178  lsatexch  35184  l1cvat  35196  lkrscss  35239  lkrss  35309  lkreqN  35311  paddunN  36067  osumcllem2N  36097  pmapojoinN  36108  pl42lem2N  36120  dibglbN  37309  diblss  37313  dicvaddcl  37333  dicvscacl  37334  diclss  37336  cdlemn5pre  37343  dihord5apre  37405  dihglblem3N  37438  dihglb2  37485  dochsat  37526  dochshpncl  37527  djhspss  37549  dihsumssj  37551  mapdlsm  37807  hdmaprnlem3eN  38004  hdmaplkr  38059  trrelsuperreldg  38211  iunrelexpuztr  38227  funfvima2d  38499
  Copyright terms: Public domain W3C validator