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

Theorem sseqtr4i 3487
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 4-Apr-1995.)
Hypotheses
Ref Expression
sseqtr4.1  |-  A  C_  B
sseqtr4.2  |-  C  =  B
Assertion
Ref Expression
sseqtr4i  |-  A  C_  C

Proof of Theorem sseqtr4i
StepHypRef Expression
1 sseqtr4.1 . 2  |-  A  C_  B
2 sseqtr4.2 . . 3  |-  C  =  B
32eqcomi 2464 . 2  |-  B  =  C
41, 3sseqtri 3486 1  |-  A  C_  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1370    C_ wss 3426
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-in 3433  df-ss 3440
This theorem is referenced by:  eqimss2i  3509  snsspr1  4120  snsspr2  4121  snsstp1  4122  snsstp2  4123  snsstp3  4124  unissint  4250  iunxdif2  4316  intabs  4551  sssucid  4894  opabssxp  5009  dmresi  5259  cnvimass  5287  ssrnres  5374  sofld  5384  cnvcnv  5388  cnvssrndm  5457  fvclss  6058  dmmpt2ssx  6739  suppun  6809  tfrlem11  6947  oawordeulem  7093  mapex  7320  trcl  8049  dfac3  8392  cfsuc  8527  fin23lem11  8587  domtriomlem  8712  ttukeylem1  8779  ttukeylem7  8785  brdom7disj  8799  brdom6disj  8800  fingch  8891  fpwwe2lem13  8910  canthp1lem2  8921  wunex2  9006  wunex3  9009  ressxr  9528  ltrelxr  9539  nnssnn0  10683  un0addcl  10714  un0mulcl  10715  fzossnn0  11681  caubnd  12948  isumclim3  13328  znnen  13597  isprm3  13874  phimullem  13956  vdwnnlem1  14158  isstruct2  14285  2strbas  14377  2strop  14378  rngbase  14388  rngplusg  14389  rngmulr  14390  srngbase  14396  srngplusg  14397  srngmulr  14398  srnginvl  14399  lmodbase  14405  lmodplusg  14406  lmodsca  14407  lmodvsca  14408  ipsbase  14412  ipsaddg  14413  ipsmulr  14414  ipssca  14415  ipsvsca  14416  ipsip  14417  phlbase  14422  phlplusg  14423  phlsca  14424  phlvsca  14425  phlip  14426  topgrpbas  14430  topgrpplusg  14431  topgrptset  14432  otpsbas  14437  otpstset  14438  otpsle  14439  odrngbas  14448  odrngplusg  14449  odrngmulr  14450  odrngtset  14451  odrngle  14452  odrngds  14453  homarw  15016  ipoval  15426  ipolerval  15428  cycsubg  15811  eqgfval  15831  gsumval3OLD  16486  gsumval3  16489  gsumzaddlemOLD  16514  islbs3  17342  cnfldbas  17931  cnfldadd  17932  cnfldmul  17933  cnfldcj  17934  cnfldtset  17935  cnfldle  17936  cnfldds  17937  cnfldunif  17938  basdif0  18674  tgdif0  18713  iscldtop  18815  iocpnfordt  18935  icomnfordt  18936  iooordt  18937  cnrest2  19006  cmpcov2  19109  fiuncmp  19123  bwth  19129  indiscon  19138  xkococnlem  19348  hmphdis  19485  uzrest  19586  ufildr  19620  fin1aufil  19621  eltsms  19819  ustval  19893  qtopbaslem  20453  tgqioo  20493  re2ndc  20494  xrhmeo  20634  bndth  20646  pi1xfrcnvlem  20744  ovolficcss  21069  nulmbl2  21134  uniiccdif  21174  opnmbllem  21197  opnmblALT  21199  mbfimaopnlem  21249  i1fima  21272  i1fima2  21273  i1fd  21275  c1liplem1  21584  deg1n0ima  21676  efcvx  22030  dvrelog  22198  dvloglem  22209  logf1o2  22211  dvlog  22212  ressatans  22445  wilthlem3  22524  trkgbas  23021  trkgdist  23022  trkgitv  23023  ex-ss  23769  ajfval  24344  ipasslem8  24372  hlimcaui  24774  shsspwh  24784  hhssabloi  24798  hhssnv  24800  hhshsslem1  24803  shunssji  24907  sshhococi  25084  pjoml6i  25127  osumcori  25181  mayete3i  25266  mayete3iOLD  25267  mayetes3i  25268  imaelshi  25597  pjclem1  25734  pjci  25739  mdcompli  25968  dmdcompli  25969  xppreima  26098  fzssnn  26208  gsummpt2co  26383  rnlogblem  26592  esumpcvgval  26661  esumcvg  26669  elmbfmvol2  26816  sxbrsigalem0  26820  eulerpartlemsv3  26878  ballotlemsup  27021  ballotlem7  27052  signswbase  27089  signswplusg  27090  subfacp1lem2a  27202  subfacp1lem2b  27203  erdszelem2  27214  kur14lem7  27234  kur14lem9  27236  fprodefsum  27619  iprodclim3  27634  dfon2lem2  27731  wfrlem14  27871  bpoly4  28336  opnmbllem0  28565  mblfinlem3  28568  mblfinlem4  28569  ismblfin  28570  volsupnfl  28574  locfincmp  28714  sdclem2  28776  heibor1lem  28846  ismrc  29175  mapfzcons1cl  29192  2rexfrabdioph  29272  3rexfrabdioph  29273  4rexfrabdioph  29274  6rexfrabdioph  29275  7rexfrabdioph  29276  rabdiophlem2  29278  jm2.27dlem5  29500  algbase  29673  algaddg  29674  algmulr  29675  algsca  29676  algvsca  29677  lhe4.4ex1a  29741  dvcosre  29926  dmmpt2ssx2  30865  nn0gsumfz  30945  pmatcollpw4fi  31241  bnj931  32064  bnj1137  32286  bj-snglsstag  32774  bj-2upln1upl  32817  bj-ccssccbar  32846  bj-ccinftyssccbar  32847  dicval  35127  dvhdimlem  35395
  Copyright terms: Public domain W3C validator