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

Theorem sseqtr4i 3530
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 2473 . 2  |-  B  =  C
41, 3sseqtri 3529 1  |-  A  C_  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1374    C_ wss 3469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-in 3476  df-ss 3483
This theorem is referenced by:  eqimss2i  3552  snsspr1  4169  snsspr2  4170  snsstp1  4171  snsstp2  4172  snsstp3  4173  unissint  4299  iunxdif2  4366  intabs  4601  sssucid  4948  opabssxp  5065  dmresi  5320  cnvimass  5348  ssrnres  5436  sofld  5446  cnvcnv  5450  cnvssrndm  5520  fvclss  6133  dmmpt2ssx  6839  suppun  6910  tfrlem11  7047  oawordeulem  7193  mapex  7416  trcl  8148  dfac3  8491  cfsuc  8626  fin23lem11  8686  domtriomlem  8811  ttukeylem1  8878  ttukeylem7  8884  brdom7disj  8898  brdom6disj  8899  fingch  8990  fpwwe2lem13  9009  canthp1lem2  9020  wunex2  9105  wunex3  9108  ressxr  9626  ltrelxr  9637  nnssnn0  10787  un0addcl  10818  un0mulcl  10819  fzossnn0  11813  caubnd  13140  isumclim3  13523  znnen  13796  isprm3  14074  phimullem  14157  vdwnnlem1  14361  isstruct2  14488  2strbas  14581  2strop  14582  rngbase  14592  rngplusg  14593  rngmulr  14594  srngbase  14600  srngplusg  14601  srngmulr  14602  srnginvl  14603  lmodbase  14609  lmodplusg  14610  lmodsca  14611  lmodvsca  14612  ipsbase  14616  ipsaddg  14617  ipsmulr  14618  ipssca  14619  ipsvsca  14620  ipsip  14621  phlbase  14626  phlplusg  14627  phlsca  14628  phlvsca  14629  phlip  14630  topgrpbas  14634  topgrpplusg  14635  topgrptset  14636  otpsbas  14641  otpstset  14642  otpsle  14643  odrngbas  14652  odrngplusg  14653  odrngmulr  14654  odrngtset  14655  odrngle  14656  odrngds  14657  homarw  15220  ipoval  15630  ipolerval  15632  cycsubg  16017  eqgfval  16037  gsumval3OLD  16692  gsumval3  16695  gsumzaddlemOLD  16720  nn0gsumfz  16796  islbs3  17577  cnfldbas  18188  cnfldadd  18189  cnfldmul  18190  cnfldcj  18191  cnfldtset  18192  cnfldle  18193  cnfldds  18194  cnfldunif  18195  pmatcollpw3fi  19046  basdif0  19214  tgdif0  19253  iscldtop  19355  iocpnfordt  19475  icomnfordt  19476  iooordt  19477  cnrest2  19546  cmpcov2  19649  fiuncmp  19663  bwth  19669  indiscon  19678  xkococnlem  19888  hmphdis  20025  uzrest  20126  ufildr  20160  fin1aufil  20161  eltsms  20359  ustval  20433  qtopbaslem  20993  tgqioo  21033  re2ndc  21034  xrhmeo  21174  bndth  21186  pi1xfrcnvlem  21284  ovolficcss  21609  nulmbl2  21675  uniiccdif  21715  opnmbllem  21738  opnmblALT  21740  mbfimaopnlem  21790  i1fima  21813  i1fima2  21814  i1fd  21816  c1liplem1  22125  deg1n0ima  22217  efcvx  22571  dvrelog  22739  dvloglem  22750  logf1o2  22752  dvlog  22753  ressatans  22986  wilthlem3  23065  trkgbas  23562  trkgdist  23563  trkgitv  23564  ex-ss  24675  ajfval  25250  ipasslem8  25278  hlimcaui  25680  shsspwh  25690  hhssabloi  25704  hhssnv  25706  hhshsslem1  25709  shunssji  25813  sshhococi  25990  pjoml6i  26033  osumcori  26087  mayete3i  26172  mayete3iOLD  26173  mayetes3i  26174  imaelshi  26503  pjclem1  26640  pjci  26645  mdcompli  26874  dmdcompli  26875  xppreima  27009  fzssnn  27113  gsummpt2co  27284  circtopn  27488  rnlogblem  27505  esumpcvgval  27574  esumcvg  27582  elmbfmvol2  27728  sxbrsigalem0  27732  eulerpartlemsv3  27790  ballotlemsup  27933  ballotlem7  27964  signswbase  28001  signswplusg  28002  subfacp1lem2a  28114  subfacp1lem2b  28115  erdszelem2  28126  kur14lem7  28146  kur14lem9  28148  fprodefsum  28531  iprodclim3  28546  dfon2lem2  28643  wfrlem14  28783  bpoly4  29248  opnmbllem0  29478  mblfinlem3  29481  mblfinlem4  29482  ismblfin  29483  volsupnfl  29487  locfincmp  29627  sdclem2  29689  heibor1lem  29759  ismrc  30088  mapfzcons1cl  30105  2rexfrabdioph  30184  3rexfrabdioph  30185  4rexfrabdioph  30186  6rexfrabdioph  30187  7rexfrabdioph  30188  rabdiophlem2  30190  jm2.27dlem5  30412  algbase  30585  algaddg  30586  algmulr  30587  algsca  30588  algvsca  30589  lhe4.4ex1a  30653  dvcosre  31058  fourierdlem46  31272  fourierdlem57  31283  fourierdlem58  31284  fourierdlem62  31288  fourierdlem102  31328  fourierdlem114  31340  dmmpt2ssx2  31865  bnj931  32783  bnj1137  33005  bj-snglsstag  33495  bj-2upln1upl  33538  bj-ccssccbar  33567  bj-ccinftyssccbar  33568  dicval  35848  dvhdimlem  36116
  Copyright terms: Public domain W3C validator