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

Theorem sseqtr4i 3384
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 2442 . 2  |-  B  =  C
41, 3sseqtri 3383 1  |-  A  C_  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1369    C_ wss 3323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3330  df-ss 3337
This theorem is referenced by:  eqimss2i  3406  snsspr1  4017  snsspr2  4018  snsstp1  4019  snsstp2  4020  snsstp3  4021  unissint  4147  iunxdif2  4213  intabs  4448  sssucid  4791  opabssxp  4906  dmresi  5156  cnvimass  5184  ssrnres  5271  sofld  5281  cnvcnv  5285  cnvssrndm  5354  fvclss  5954  dmmpt2ssx  6634  suppun  6704  tfrlem11  6839  oawordeulem  6985  mapex  7212  trcl  7940  dfac3  8283  cfsuc  8418  fin23lem11  8478  domtriomlem  8603  ttukeylem1  8670  ttukeylem7  8676  brdom7disj  8690  brdom6disj  8691  fingch  8782  fpwwe2lem13  8801  canthp1lem2  8812  wunex2  8897  wunex3  8900  ressxr  9419  ltrelxr  9430  nnssnn0  10574  un0addcl  10605  un0mulcl  10606  fzossnn0  11572  caubnd  12838  isumclim3  13218  znnen  13487  isprm3  13764  phimullem  13846  vdwnnlem1  14048  isstruct2  14175  2strbas  14267  2strop  14268  rngbase  14278  rngplusg  14279  rngmulr  14280  srngbase  14286  srngplusg  14287  srngmulr  14288  srnginvl  14289  lmodbase  14295  lmodplusg  14296  lmodsca  14297  lmodvsca  14298  ipsbase  14302  ipsaddg  14303  ipsmulr  14304  ipssca  14305  ipsvsca  14306  ipsip  14307  phlbase  14312  phlplusg  14313  phlsca  14314  phlvsca  14315  phlip  14316  topgrpbas  14320  topgrpplusg  14321  topgrptset  14322  otpsbas  14327  otpstset  14328  otpsle  14329  odrngbas  14338  odrngplusg  14339  odrngmulr  14340  odrngtset  14341  odrngle  14342  odrngds  14343  homarw  14906  ipoval  15316  ipolerval  15318  cycsubg  15700  eqgfval  15720  gsumval3OLD  16373  gsumval3  16376  gsumzaddlemOLD  16401  islbs3  17216  cnfldbas  17802  cnfldadd  17803  cnfldmul  17804  cnfldcj  17805  cnfldtset  17806  cnfldle  17807  cnfldds  17808  cnfldunif  17809  basdif0  18538  tgdif0  18577  iscldtop  18679  iocpnfordt  18799  icomnfordt  18800  iooordt  18801  cnrest2  18870  cmpcov2  18973  fiuncmp  18987  bwth  18993  indiscon  19002  xkococnlem  19212  hmphdis  19349  uzrest  19450  ufildr  19484  fin1aufil  19485  eltsms  19683  ustval  19757  qtopbaslem  20317  tgqioo  20357  re2ndc  20358  xrhmeo  20498  bndth  20510  pi1xfrcnvlem  20608  ovolficcss  20933  nulmbl2  20998  uniiccdif  21038  opnmbllem  21061  opnmblALT  21063  mbfimaopnlem  21113  i1fima  21136  i1fima2  21137  i1fd  21139  c1liplem1  21448  deg1n0ima  21540  efcvx  21894  dvrelog  22062  dvloglem  22073  logf1o2  22075  dvlog  22076  ressatans  22309  wilthlem3  22388  trkgbas  22886  trkgdist  22887  trkgitv  22888  ex-ss  23602  ajfval  24177  ipasslem8  24205  hlimcaui  24607  shsspwh  24617  hhssabloi  24631  hhssnv  24633  hhshsslem1  24636  shunssji  24740  sshhococi  24917  pjoml6i  24960  osumcori  25014  mayete3i  25099  mayete3iOLD  25100  mayetes3i  25101  imaelshi  25430  pjclem1  25567  pjci  25572  mdcompli  25801  dmdcompli  25802  xppreima  25932  fzssnn  26042  gsummpt2co  26217  rnlogblem  26427  esumpcvgval  26496  esumcvg  26504  elmbfmvol2  26651  sxbrsigalem0  26655  eulerpartlemsv3  26713  ballotlemsup  26856  ballotlem7  26887  signswbase  26924  signswplusg  26925  subfacp1lem2a  27037  subfacp1lem2b  27038  erdszelem2  27049  kur14lem7  27069  kur14lem9  27071  fprodefsum  27454  iprodclim3  27469  dfon2lem2  27566  wfrlem14  27706  bpoly4  28171  opnmbllem0  28398  mblfinlem3  28401  mblfinlem4  28402  ismblfin  28403  volsupnfl  28407  locfincmp  28547  sdclem2  28609  heibor1lem  28679  ismrc  29008  mapfzcons1cl  29025  2rexfrabdioph  29105  3rexfrabdioph  29106  4rexfrabdioph  29107  6rexfrabdioph  29108  7rexfrabdioph  29109  rabdiophlem2  29111  jm2.27dlem5  29333  algbase  29506  algaddg  29507  algmulr  29508  algsca  29509  algvsca  29510  lhe4.4ex1a  29574  dvcosre  29759  dmmpt2ssx2  30697  nn0gsumfz  30773  bnj931  31693  bnj1137  31915  bj-snglsstag  32374  bj-2upln1upl  32417  bj-ccssccbar  32440  bj-ccinftyssccbar  32441  dicval  34714  dvhdimlem  34982
  Copyright terms: Public domain W3C validator