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

Theorem sseqtr4i 3475
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 2415 . 2  |-  B  =  C
41, 3sseqtri 3474 1  |-  A  C_  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1405    C_ wss 3414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-in 3421  df-ss 3428
This theorem is referenced by:  eqimss2i  3497  snsspr1  4121  snsspr2  4122  snsstp1  4123  snsstp2  4124  snsstp3  4125  unissint  4252  iunxdif2  4319  intabs  4555  opabssxp  4898  dmresi  5149  cnvimass  5177  ssrnres  5263  sofld  5272  cnvcnv  5276  cnvssrndm  5345  sssucid  5487  fvclss  6135  dmmpt2ssx  6849  suppun  6923  wfrlem14  7034  tfrlem11  7091  oawordeulem  7240  mapex  7463  trcl  8191  dfac3  8534  cfsuc  8669  fin23lem11  8729  domtriomlem  8854  ttukeylem1  8921  ttukeylem7  8927  brdom7disj  8941  brdom6disj  8942  fingch  9031  fpwwe2lem13  9050  canthp1lem2  9061  wunex2  9146  wunex3  9149  ressxr  9667  ltrelxr  9678  nnssnn0  10839  un0addcl  10870  un0mulcl  10871  fzossnn0  11888  caubnd  13340  isumclim3  13725  iprodclim3  13945  bpoly4  14004  fprodefsum  14039  znnen  14155  isprm3  14435  phimullem  14518  vdwnnlem1  14722  isstruct2  14850  2strbas  14950  2strop  14951  rngbase  14961  rngplusg  14962  rngmulr  14963  srngbase  14969  srngplusg  14970  srngmulr  14971  srnginvl  14972  lmodbase  14978  lmodplusg  14979  lmodsca  14980  lmodvsca  14981  ipsbase  14985  ipsaddg  14986  ipsmulr  14987  ipssca  14988  ipsvsca  14989  ipsip  14990  phlbase  14995  phlplusg  14996  phlsca  14997  phlvsca  14998  phlip  14999  topgrpbas  15003  topgrpplusg  15004  topgrptset  15005  otpsbas  15010  otpstset  15011  otpsle  15012  odrngbas  15021  odrngplusg  15022  odrngmulr  15023  odrngtset  15024  odrngle  15025  odrngds  15026  homarw  15649  ipoval  16108  ipolerval  16110  cycsubg  16553  eqgfval  16573  gsumval3OLD  17232  gsumval3  17235  gsumzaddlemOLD  17260  nn0gsumfz  17332  islbs3  18121  cnfldbas  18744  cnfldadd  18745  cnfldmul  18746  cnfldcj  18747  cnfldtset  18748  cnfldle  18749  cnfldds  18750  cnfldunif  18751  pmatcollpw3fi  19578  basdif0  19746  iscldtop  19889  iocpnfordt  20009  icomnfordt  20010  iooordt  20011  cnrest2  20080  cmpcov2  20183  fiuncmp  20197  bwth  20203  indiscon  20211  locfincmp  20319  xkococnlem  20452  hmphdis  20589  uzrest  20690  ufildr  20724  fin1aufil  20725  eltsms  20923  ustval  20997  qtopbaslem  21557  tgqioo  21597  re2ndc  21598  xrhmeo  21738  bndth  21750  pi1xfrcnvlem  21848  ovolficcss  22173  nulmbl2  22239  uniiccdif  22279  opnmbllem  22302  opnmblALT  22304  mbfimaopnlem  22354  i1fima  22377  i1fima2  22378  i1fd  22380  c1liplem1  22689  deg1n0ima  22781  efcvx  23136  dvrelog  23312  dvloglem  23323  logf1o2  23325  dvlog  23326  ressatans  23590  wilthlem3  23725  trkgbas  24221  trkgdist  24222  trkgitv  24223  ex-ss  25565  ajfval  26138  ipasslem8  26166  hlimcaui  26568  shsspwh  26578  hhssabloi  26592  hhssnv  26594  hhshsslem1  26597  shunssji  26701  sshhococi  26878  pjoml6i  26921  osumcori  26975  mayete3i  27060  mayetes3i  27061  imaelshi  27390  pjclem1  27527  pjci  27532  mdcompli  27761  dmdcompli  27762  xppreima  27930  fzssnn  28043  gsummpt2co  28222  circtopn  28293  esumpcvgval  28525  esumcvg  28533  ldgenpisyslem3  28613  elmbfmvol2  28715  sxbrsigalem0  28719  eulerpartlemsv3  28806  ballotlemsup  28949  ballotlem7  28980  bnj931  29156  bnj1137  29378  subfacp1lem2a  29477  subfacp1lem2b  29478  erdszelem2  29489  kur14lem7  29509  kur14lem9  29511  dfon2lem2  30003  bj-snglsstag  31104  bj-2upln1upl  31147  bj-ccssccbar  31184  bj-ccinftyssccbar  31185  icoreelrn  31278  opnmbllem0  31422  mblfinlem3  31425  mblfinlem4  31426  ismblfin  31427  volsupnfl  31431  sdclem2  31517  heibor1lem  31587  dicval  34196  dvhdimlem  34464  ismrc  34995  mapfzcons1cl  35012  2rexfrabdioph  35091  3rexfrabdioph  35092  4rexfrabdioph  35093  6rexfrabdioph  35094  7rexfrabdioph  35095  rabdiophlem2  35097  jm2.27dlem5  35317  algbase  35491  algaddg  35492  algmulr  35493  algsca  35494  algvsca  35495  intimass2  35634  comptiunov2i  35685  relexp0a  35695  lhe4.4ex1a  36082  dvcosre  37074  fourierdlem46  37303  fourierdlem57  37314  fourierdlem58  37315  fourierdlem62  37319  fourierdlem102  37359  fourierdlem103  37360  fourierdlem104  37361  fourierdlem114  37371  dmmpt2ssx2  38437  aacllem  38860
  Copyright terms: Public domain W3C validator