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

Theorem sseqtr4i 3465
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 2460 . 2  |-  B  =  C
41, 3sseqtri 3464 1  |-  A  C_  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1444    C_ wss 3404
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-in 3411  df-ss 3418
This theorem is referenced by:  eqimss2i  3487  snsspr1  4121  snsspr2  4122  snsstp1  4123  snsstp2  4124  snsstp3  4125  unissint  4259  iunxdif2  4326  intabs  4564  opabssxp  4909  dmresi  5160  cnvimass  5188  ssrnres  5275  sofld  5284  cnvcnv  5288  cnvssrndm  5357  sssucid  5500  fvclss  6147  dmmpt2ssx  6858  suppun  6935  wfrlem14  7049  tfrlem11  7106  oawordeulem  7255  mapex  7478  trcl  8212  dfac3  8552  cfsuc  8687  fin23lem11  8747  domtriomlem  8872  ttukeylem1  8939  ttukeylem7  8945  brdom7disj  8959  brdom6disj  8960  fingch  9048  fpwwe2lem13  9067  canthp1lem2  9078  wunex2  9163  wunex3  9166  ressxr  9684  ltrelxr  9695  nnssnn0  10872  un0addcl  10903  un0mulcl  10904  fzssnn  11842  fzossnn0  11949  caubnd  13421  isumclim3  13820  iprodclim3  14053  bpoly4  14112  fprodefsum  14149  znnen  14265  isprm3  14633  phimullem  14727  vdwnnlem1  14945  isstruct2  15130  2strbas  15231  2strop  15232  2strbas1  15234  rngbase  15245  rngplusg  15246  rngmulr  15247  srngbase  15253  srngplusg  15254  srngmulr  15255  srnginvl  15256  lmodbase  15262  lmodplusg  15263  lmodsca  15264  lmodvsca  15265  ipsbase  15269  ipsaddg  15270  ipsmulr  15271  ipssca  15272  ipsvsca  15273  ipsip  15274  phlbase  15279  phlplusg  15280  phlsca  15281  phlvsca  15282  phlip  15283  topgrpbas  15287  topgrpplusg  15288  topgrptset  15289  otpsbas  15294  otpstset  15295  otpsle  15296  odrngbas  15305  odrngplusg  15306  odrngmulr  15307  odrngtset  15308  odrngle  15309  odrngds  15310  homarw  15941  ipoval  16400  ipolerval  16402  cycsubg  16845  eqgfval  16865  gsumval3  17541  nn0gsumfz  17613  islbs3  18378  cnfldbas  18974  cnfldadd  18975  cnfldmul  18976  cnfldcj  18977  cnfldtset  18978  cnfldle  18979  cnfldds  18980  cnfldunif  18981  pmatcollpw3fi  19809  basdif0  19968  iscldtop  20111  iocpnfordt  20231  icomnfordt  20232  iooordt  20233  cnrest2  20302  cmpcov2  20405  fiuncmp  20419  bwth  20425  indiscon  20433  locfincmp  20541  xkococnlem  20674  hmphdis  20811  uzrest  20912  ufildr  20946  fin1aufil  20947  eltsms  21147  ustval  21217  qtopbaslem  21779  tgqioo  21818  re2ndc  21819  xrhmeo  21974  bndth  21986  pi1xfrcnvlem  22087  ovolficcss  22422  nulmbl2  22490  uniiccdif  22535  opnmbllem  22559  opnmblALT  22561  mbfimaopnlem  22611  i1fima  22636  i1fima2  22637  i1fd  22639  c1liplem1  22948  deg1n0ima  23038  efcvx  23404  dvrelog  23582  dvloglem  23593  logf1o2  23595  dvlog  23596  ressatans  23860  wilthlem3  23995  trkgbas  24493  trkgdist  24494  trkgitv  24495  ex-ss  25877  ajfval  26450  ipasslem8  26478  hlimcaui  26889  shsspwh  26899  hhssabloi  26913  hhssnv  26915  hhshsslem1  26918  shunssji  27022  sshhococi  27199  pjoml6i  27242  osumcori  27296  mayete3i  27381  mayetes3i  27382  imaelshi  27711  pjclem1  27848  pjci  27853  mdcompli  28082  dmdcompli  28083  xppreima  28248  gsummpt2co  28543  circtopn  28664  esumpcvgval  28899  esumcvg  28907  ldgenpisyslem3  28987  elmbfmvol2  29089  sxbrsigalem0  29093  eulerpartlemsv3  29194  ballotlem7  29368  ballotlemsupOLD  29375  ballotlem7OLD  29406  bnj931  29582  bnj1137  29804  subfacp1lem2a  29903  subfacp1lem2b  29904  erdszelem2  29915  kur14lem7  29935  kur14lem9  29937  dfon2lem2  30430  bj-snglsstag  31575  bj-2upln1upl  31618  bj-ccssccbar  31659  bj-ccinftyssccbar  31660  icoreelrn  31764  finxpreclem3  31785  imadifss  31928  poimirlem4  31944  poimirlem26  31966  poimirlem27  31967  opnmbllem0  31976  mblfinlem3  31979  mblfinlem4  31980  ismblfin  31981  volsupnfl  31985  sdclem2  32071  heibor1lem  32141  dicval  34744  dvhdimlem  35012  ismrc  35543  mapfzcons1cl  35560  2rexfrabdioph  35639  3rexfrabdioph  35640  4rexfrabdioph  35641  6rexfrabdioph  35642  7rexfrabdioph  35643  rabdiophlem2  35645  jm2.27dlem5  35868  algbase  36044  algaddg  36045  algmulr  36046  algsca  36047  algvsca  36048  intimass2  36247  comptiunov2i  36298  relexp0a  36308  lhe4.4ex1a  36678  iocnct  37642  iccnct  37643  dvcosre  37781  fourierdlem46  38016  fourierdlem57  38027  fourierdlem58  38028  fourierdlem62  38032  fourierdlem102  38072  fourierdlem103  38073  fourierdlem104  38074  fourierdlem114  38084  sge0split  38251  sge0uzfsumgt  38286  hoiprodp1  38410  hoidmvlelem1  38417  hoidmvlelem2  38418  hoidmvlelem3  38419  nn0ssxnn0  39073  dmmpt2ssx2  40171  aacllem  40593
  Copyright terms: Public domain W3C validator