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

Theorem sseqtr4i 3600
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 4-Apr-1995.)
Hypotheses
Ref Expression
sseqtr4.1 𝐴𝐵
sseqtr4.2 𝐶 = 𝐵
Assertion
Ref Expression
sseqtr4i 𝐴𝐶

Proof of Theorem sseqtr4i
StepHypRef Expression
1 sseqtr4.1 . 2 𝐴𝐵
2 sseqtr4.2 . . 3 𝐶 = 𝐵
32eqcomi 2618 . 2 𝐵 = 𝐶
41, 3sseqtri 3599 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  wss 3539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-in 3546  df-ss 3553
This theorem is referenced by:  eqimss2i  3622  snsspr1  4284  snsspr2  4285  snsstp1  4286  snsstp2  4287  snsstp3  4288  unissint  4430  iunxdif2  4498  intabs  4747  opabssxp  5106  dmresi  5363  cnvimass  5391  ssrnres  5477  sofld  5486  cnvcnv  5491  cnvssrndm  5560  sssucid  5705  fvclss  6382  dmmpt2ssx  7101  suppun  7179  wfrlem14  7292  tfrlem11  7348  oawordeulem  7498  mapex  7727  trcl  8464  dfac3  8804  cfsuc  8939  fin23lem11  8999  domtriomlem  9124  ttukeylem1  9191  ttukeylem7  9197  brdom7disj  9211  brdom6disj  9212  fingch  9301  fpwwe2lem13  9320  canthp1lem2  9331  wunex2  9416  wunex3  9419  ressxr  9939  ltrelxr  9950  nnssnn0  11142  un0addcl  11173  un0mulcl  11174  fzssnn  12211  caubnd  13892  isumclim3  14278  iprodclim3  14516  bpoly4  14575  fprodefsum  14610  znnen  14726  isprm3  15180  phimullem  15268  vdwnnlem1  15483  isstruct2  15650  2strbas  15756  2strop  15757  2strbas1  15759  rngbase  15770  rngplusg  15771  rngmulr  15772  srngbase  15778  srngplusg  15779  srngmulr  15780  srnginvl  15781  lmodbase  15787  lmodplusg  15788  lmodsca  15789  lmodvsca  15790  ipsbase  15794  ipsaddg  15795  ipsmulr  15796  ipssca  15797  ipsvsca  15798  ipsip  15799  phlbase  15804  phlplusg  15805  phlsca  15806  phlvsca  15807  phlip  15808  topgrpbas  15812  topgrpplusg  15813  topgrptset  15814  otpsbas  15821  otpstset  15822  otpsle  15823  otpsbasOLD  15825  otpstsetOLD  15826  otpsleOLD  15827  odrngbas  15836  odrngplusg  15837  odrngmulr  15838  odrngtset  15839  odrngle  15840  odrngds  15841  homarw  16465  ipoval  16923  ipolerval  16925  cycsubg  17391  eqgfval  17411  gsumval3  18077  islbs3  18922  cnfldbas  19517  cnfldadd  19518  cnfldmul  19519  cnfldcj  19520  cnfldtset  19521  cnfldle  19522  cnfldds  19523  cnfldunif  19524  basdif0  20510  iscldtop  20651  iocpnfordt  20771  icomnfordt  20772  iooordt  20773  cnrest2  20842  cmpcov2  20945  fiuncmp  20959  bwth  20965  indiscon  20973  locfincmp  21081  xkococnlem  21214  hmphdis  21351  uzrest  21453  ufildr  21487  fin1aufil  21488  eltsms  21688  ustval  21758  qtopbaslem  22304  tgqioo  22343  re2ndc  22344  xrhmeo  22484  bndth  22496  pi1xfrcnvlem  22595  ovolficcss  22962  nulmbl2  23028  uniiccdif  23069  opnmbllem  23092  opnmblALT  23094  mbfimaopnlem  23145  i1fima  23168  i1fima2  23169  i1fd  23171  c1liplem1  23480  deg1n0ima  23570  efcvx  23924  dvrelog  24100  dvloglem  24111  logf1o2  24113  dvlog  24114  ressatans  24378  wilthlem3  24513  trkgbas  25061  trkgdist  25062  trkgitv  25063  ex-ss  26442  ajfval  26854  ipasslem8  26882  hlimcaui  27283  shsspwh  27293  hhssabloi  27309  hhssnv  27311  hhshsslem1  27314  shunssji  27418  sshhococi  27595  pjoml6i  27638  osumcori  27692  mayete3i  27777  mayetes3i  27778  imaelshi  28107  pjclem1  28244  pjci  28249  mdcompli  28478  dmdcompli  28479  xppreima  28635  gsummpt2co  28917  circtopn  29038  esumpcvgval  29273  esumcvg  29281  ldgenpisyslem3  29361  elmbfmvol2  29462  sxbrsigalem0  29466  eulerpartlemsv3  29556  ballotlem7  29730  bnj931  29901  bnj1137  30123  subfacp1lem2a  30222  subfacp1lem2b  30223  erdszelem2  30234  kur14lem7  30254  kur14lem9  30256  dfon2lem2  30739  bj-snglsstag  31958  bj-2upln1upl  32001  bj-ccssccbar  32077  bj-ccinftyssccbar  32078  icoreelrn  32181  finxpreclem3  32202  imadifss  32350  poimirlem4  32379  poimirlem26  32401  poimirlem27  32402  opnmbllem0  32411  mblfinlem3  32414  mblfinlem4  32415  ismblfin  32416  volsupnfl  32420  sdclem2  32504  heibor1lem  32574  dicval  35279  dvhdimlem  35547  ismrc  36078  mapfzcons1cl  36095  2rexfrabdioph  36174  3rexfrabdioph  36175  4rexfrabdioph  36176  6rexfrabdioph  36177  7rexfrabdioph  36178  rabdiophlem2  36180  jm2.27dlem5  36394  algbase  36563  algaddg  36564  algmulr  36565  algsca  36566  algvsca  36567  intimass2  36762  comptiunov2i  36813  relexp0a  36823  lhe4.4ex1a  37346  iocnct  38411  iccnct  38412  dvcosre  38596  fourierdlem46  38842  fourierdlem57  38853  fourierdlem58  38854  fourierdlem62  38858  fourierdlem102  38898  fourierdlem103  38899  fourierdlem104  38900  fourierdlem114  38910  sge0split  39099  sge0uzfsumgt  39134  hoiprodp1  39275  hoidmvlelem1  39282  hoidmvlelem2  39283  hoidmvlelem3  39284  nn0ssxnn0  40195  dmmpt2ssx2  41903  aacllem  42312
  Copyright terms: Public domain W3C validator