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

Theorem sseqtr4i 3623
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 2630 . 2 𝐵 = 𝐶
41, 3sseqtri 3622 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  wss 3560
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-in 3567  df-ss 3574
This theorem is referenced by:  eqimss2i  3645  snsspr1  4320  snsspr2  4321  snsstp1  4322  snsstp2  4323  snsstp3  4324  unissint  4473  iunxdif2  4541  pwpwssunieq  4588  intabs  4795  opabssxp  5164  dmresi  5426  cnvimass  5454  ssrnres  5541  sofld  5550  cnvcnv  5555  cnvcnvOLD  5556  cnvssrndm  5626  sssucid  5771  fvclss  6465  dmmpt2ssx  7195  suppun  7275  wfrlem14  7388  tfrlem11  7444  oawordeulem  7594  mapex  7823  trcl  8564  dfac3  8904  cfsuc  9039  fin23lem11  9099  domtriomlem  9224  ttukeylem1  9291  ttukeylem7  9297  brdom7disj  9313  brdom6disj  9314  fingch  9405  fpwwe2lem13  9424  canthp1lem2  9435  wunex2  9520  wunex3  9523  ressxr  10043  ltrelxr  10059  nnssnn0  11255  un0addcl  11286  un0mulcl  11287  nn0ssxnn0  11326  fzssnn  12343  caubnd  14048  isumclim3  14437  iprodclim3  14675  bpoly4  14734  fprodefsum  14769  znnen  14885  isprm3  15339  phimullem  15427  vdwnnlem1  15642  isstruct2  15809  2strbas  15924  2strop  15925  2strbas1  15927  rngbase  15941  rngplusg  15942  rngmulr  15943  srngbase  15949  srngplusg  15950  srngmulr  15951  srnginvl  15952  lmodbase  15958  lmodplusg  15959  lmodsca  15960  lmodvsca  15961  ipsbase  15965  ipsaddg  15966  ipsmulr  15967  ipssca  15968  ipsvsca  15969  ipsip  15970  phlbase  15975  phlplusg  15976  phlsca  15977  phlvsca  15978  phlip  15979  topgrpbas  15983  topgrpplusg  15984  topgrptset  15985  otpsbas  15992  otpstset  15993  otpsle  15994  otpsbasOLD  15996  otpstsetOLD  15997  otpsleOLD  15998  odrngbas  16007  odrngplusg  16008  odrngmulr  16009  odrngtset  16010  odrngle  16011  odrngds  16012  homarw  16636  ipoval  17094  ipolerval  17096  cycsubg  17562  eqgfval  17582  gsumval3  18248  islbs3  19095  cnfldbas  19690  cnfldadd  19691  cnfldmul  19692  cnfldcj  19693  cnfldtset  19694  cnfldle  19695  cnfldds  19696  cnfldunif  19697  basdif0  20697  iscldtop  20839  iocpnfordt  20959  icomnfordt  20960  iooordt  20961  cnrest2  21030  cmpcov2  21133  fiuncmp  21147  bwth  21153  indisconn  21161  locfincmp  21269  xkococnlem  21402  hmphdis  21539  uzrest  21641  ufildr  21675  fin1aufil  21676  eltsms  21876  ustval  21946  qtopbaslem  22502  tgqioo  22543  re2ndc  22544  xrhmeo  22685  bndth  22697  pi1xfrcnvlem  22796  ovolficcss  23178  nulmbl2  23244  uniiccdif  23286  opnmbllem  23309  opnmblALT  23311  mbfimaopnlem  23362  i1fima  23385  i1fima2  23386  i1fd  23388  c1liplem1  23697  deg1n0ima  23787  efcvx  24141  dvrelog  24317  dvloglem  24328  logf1o2  24330  dvlog  24331  ressatans  24595  wilthlem3  24730  trkgbas  25278  trkgdist  25279  trkgitv  25280  ex-ss  27172  ajfval  27552  ipasslem8  27580  hlimcaui  27981  shsspwh  27991  hhssabloi  28007  hhssnv  28009  hhshsslem1  28012  shunssji  28116  sshhococi  28293  pjoml6i  28336  osumcori  28390  mayete3i  28475  mayetes3i  28476  imaelshi  28805  pjclem1  28942  pjci  28947  mdcompli  29176  dmdcompli  29177  xppreima  29332  gsummpt2co  29607  circtopn  29728  esumpcvgval  29963  esumcvg  29971  ldgenpisyslem3  30051  elmbfmvol2  30152  sxbrsigalem0  30156  eulerpartlemsv3  30246  ballotlem7  30420  bnj931  30602  bnj1137  30824  subfacp1lem2a  30923  subfacp1lem2b  30924  erdszelem2  30935  kur14lem7  30955  kur14lem9  30957  dfon2lem2  31443  bj-snglsstag  32669  bj-2upln1upl  32712  bj-ccssccbar  32776  bj-ccinftyssccbar  32777  icoreelrn  32880  finxpreclem3  32901  imadifss  33055  poimirlem4  33084  poimirlem26  33106  poimirlem27  33107  opnmbllem0  33116  mblfinlem3  33119  mblfinlem4  33120  ismblfin  33121  volsupnfl  33125  sdclem2  33209  heibor1lem  33279  dicval  35984  dvhdimlem  36252  ismrc  36783  mapfzcons1cl  36800  2rexfrabdioph  36879  3rexfrabdioph  36880  4rexfrabdioph  36881  6rexfrabdioph  36882  7rexfrabdioph  36883  rabdiophlem2  36885  jm2.27dlem5  37099  algbase  37268  algaddg  37269  algmulr  37270  algsca  37271  algvsca  37272  intimass2  37467  comptiunov2i  37518  relexp0a  37528  lhe4.4ex1a  38049  iocnct  39213  iccnct  39214  dvcosre  39461  fourierdlem46  39706  fourierdlem57  39717  fourierdlem58  39718  fourierdlem62  39722  fourierdlem102  39762  fourierdlem103  39763  fourierdlem104  39764  fourierdlem114  39774  sge0split  39963  sge0uzfsumgt  39998  hoiprodp1  40139  hoidmvlelem1  40146  hoidmvlelem2  40147  hoidmvlelem3  40148  dmmpt2ssx2  41433  aacllem  41880
  Copyright terms: Public domain W3C validator