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

Theorem sseqtr4i 3519
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 2454 . 2  |-  B  =  C
41, 3sseqtri 3518 1  |-  A  C_  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1381    C_ wss 3458
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-in 3465  df-ss 3472
This theorem is referenced by:  eqimss2i  3541  snsspr1  4160  snsspr2  4161  snsstp1  4162  snsstp2  4163  snsstp3  4164  unissint  4292  iunxdif2  4359  intabs  4594  sssucid  4941  opabssxp  5060  dmresi  5315  cnvimass  5343  ssrnres  5431  sofld  5441  cnvcnv  5445  cnvssrndm  5515  fvclss  6135  dmmpt2ssx  6846  suppun  6918  tfrlem11  7055  oawordeulem  7201  mapex  7424  trcl  8157  dfac3  8500  cfsuc  8635  fin23lem11  8695  domtriomlem  8820  ttukeylem1  8887  ttukeylem7  8893  brdom7disj  8907  brdom6disj  8908  fingch  8999  fpwwe2lem13  9018  canthp1lem2  9029  wunex2  9114  wunex3  9117  ressxr  9635  ltrelxr  9646  nnssnn0  10799  un0addcl  10830  un0mulcl  10831  fzossnn0  11830  caubnd  13165  isumclim3  13548  znnen  13818  isprm3  14098  phimullem  14181  vdwnnlem1  14385  isstruct2  14513  2strbas  14606  2strop  14607  rngbase  14617  rngplusg  14618  rngmulr  14619  srngbase  14625  srngplusg  14626  srngmulr  14627  srnginvl  14628  lmodbase  14634  lmodplusg  14635  lmodsca  14636  lmodvsca  14637  ipsbase  14641  ipsaddg  14642  ipsmulr  14643  ipssca  14644  ipsvsca  14645  ipsip  14646  phlbase  14651  phlplusg  14652  phlsca  14653  phlvsca  14654  phlip  14655  topgrpbas  14659  topgrpplusg  14660  topgrptset  14661  otpsbas  14666  otpstset  14667  otpsle  14668  odrngbas  14677  odrngplusg  14678  odrngmulr  14679  odrngtset  14680  odrngle  14681  odrngds  14682  homarw  15242  ipoval  15653  ipolerval  15655  cycsubg  16098  eqgfval  16118  gsumval3OLD  16777  gsumval3  16780  gsumzaddlemOLD  16805  nn0gsumfz  16881  islbs3  17669  cnfldbas  18292  cnfldadd  18293  cnfldmul  18294  cnfldcj  18295  cnfldtset  18296  cnfldle  18297  cnfldds  18298  cnfldunif  18299  pmatcollpw3fi  19153  basdif0  19321  iscldtop  19462  iocpnfordt  19582  icomnfordt  19583  iooordt  19584  cnrest2  19653  cmpcov2  19756  fiuncmp  19770  bwth  19776  indiscon  19785  locfincmp  19893  xkococnlem  20026  hmphdis  20163  uzrest  20264  ufildr  20298  fin1aufil  20299  eltsms  20497  ustval  20571  qtopbaslem  21131  tgqioo  21171  re2ndc  21172  xrhmeo  21312  bndth  21324  pi1xfrcnvlem  21422  ovolficcss  21747  nulmbl2  21813  uniiccdif  21853  opnmbllem  21876  opnmblALT  21878  mbfimaopnlem  21928  i1fima  21951  i1fima2  21952  i1fd  21954  c1liplem1  22263  deg1n0ima  22355  efcvx  22709  dvrelog  22883  dvloglem  22894  logf1o2  22896  dvlog  22897  ressatans  23130  wilthlem3  23209  trkgbas  23706  trkgdist  23707  trkgitv  23708  ex-ss  25013  ajfval  25589  ipasslem8  25617  hlimcaui  26019  shsspwh  26029  hhssabloi  26043  hhssnv  26045  hhshsslem1  26048  shunssji  26152  sshhococi  26329  pjoml6i  26372  osumcori  26426  mayete3i  26511  mayete3iOLD  26512  mayetes3i  26513  imaelshi  26842  pjclem1  26979  pjci  26984  mdcompli  27213  dmdcompli  27214  xppreima  27352  fzssnn  27460  circtopn  27706  esumpcvgval  27950  esumcvg  27958  elmbfmvol2  28104  sxbrsigalem0  28108  eulerpartlemsv3  28166  ballotlemsup  28309  ballotlem7  28340  subfacp1lem2a  28490  subfacp1lem2b  28491  erdszelem2  28502  kur14lem7  28522  kur14lem9  28524  fprodefsum  29072  iprodclim3  29087  dfon2lem2  29184  wfrlem14  29324  bpoly4  29789  opnmbllem0  30018  mblfinlem3  30021  mblfinlem4  30022  ismblfin  30023  volsupnfl  30027  sdclem2  30203  heibor1lem  30273  ismrc  30601  mapfzcons1cl  30618  2rexfrabdioph  30697  3rexfrabdioph  30698  4rexfrabdioph  30699  6rexfrabdioph  30700  7rexfrabdioph  30701  rabdiophlem2  30703  jm2.27dlem5  30923  algbase  31096  algaddg  31097  algmulr  31098  algsca  31099  algvsca  31100  lhe4.4ex1a  31203  dvcosre  31606  fourierdlem46  31820  fourierdlem57  31831  fourierdlem58  31832  fourierdlem62  31836  fourierdlem102  31876  fourierdlem103  31877  fourierdlem104  31878  fourierdlem114  31888  dmmpt2ssx2  32634  bnj931  33536  bnj1137  33758  bj-snglsstag  34251  bj-2upln1upl  34294  bj-ccssccbar  34322  bj-ccinftyssccbar  34323  dicval  36605  dvhdimlem  36873
  Copyright terms: Public domain W3C validator