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

Theorem sseqtr4i 3671
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 2660 . 2 𝐵 = 𝐶
41, 3sseqtri 3670 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621
This theorem is referenced by:  eqimss2i  3693  snsspr1  4377  snsspr2  4378  snsstp1  4379  snsstp2  4380  snsstp3  4381  unissint  4533  iunxdif2  4600  pwpwssunieq  4647  intabs  4855  opabssxp  5227  dmresi  5492  cnvimass  5520  ssrnres  5607  sofld  5616  cnvcnv  5621  cnvcnvOLD  5622  cnvssrndm  5695  sssucid  5840  fvclss  6540  dmmpt2ssx  7280  suppun  7360  wfrlem14  7473  tfrlem11  7529  oawordeulem  7679  mapex  7905  trcl  8642  dfac3  8982  cfsuc  9117  fin23lem11  9177  domtriomlem  9302  ttukeylem1  9369  ttukeylem7  9375  brdom7disj  9391  brdom6disj  9392  fingch  9483  fpwwe2lem13  9502  canthp1lem2  9513  wunex2  9598  wunex3  9601  ressxr  10121  ltrelxr  10137  nnssnn0  11333  un0addcl  11364  un0mulcl  11365  nn0ssxnn0  11404  fzssnn  12423  caubnd  14142  isumclim3  14534  iprodclim3  14775  bpoly4  14834  fprodefsum  14869  znnen  14985  isprm3  15443  phimullem  15531  vdwnnlem1  15746  isstruct2  15914  2strbas  16031  2strop  16032  2strbas1  16034  rngbase  16048  rngplusg  16049  rngmulr  16050  srngbase  16056  srngplusg  16057  srngmulr  16058  srnginvl  16059  lmodbase  16065  lmodplusg  16066  lmodsca  16067  lmodvsca  16068  ipsbase  16072  ipsaddg  16073  ipsmulr  16074  ipssca  16075  ipsvsca  16076  ipsip  16077  phlbase  16082  phlplusg  16083  phlsca  16084  phlvsca  16085  phlip  16086  topgrpbas  16090  topgrpplusg  16091  topgrptset  16092  otpsbas  16099  otpstset  16100  otpsle  16101  otpsbasOLD  16103  otpstsetOLD  16104  otpsleOLD  16105  odrngbas  16114  odrngplusg  16115  odrngmulr  16116  odrngtset  16117  odrngle  16118  odrngds  16119  homarw  16743  ipoval  17201  ipolerval  17203  cycsubg  17669  eqgfval  17689  gsumval3  18354  islbs3  19203  cnfldbas  19798  cnfldadd  19799  cnfldmul  19800  cnfldcj  19801  cnfldtset  19802  cnfldle  19803  cnfldds  19804  cnfldunif  19805  basdif0  20805  iscldtop  20947  iocpnfordt  21067  icomnfordt  21068  iooordt  21069  cnrest2  21138  cmpcov2  21241  fiuncmp  21255  bwth  21261  indisconn  21269  locfincmp  21377  xkococnlem  21510  hmphdis  21647  uzrest  21748  ufildr  21782  fin1aufil  21783  eltsms  21983  ustval  22053  qtopbaslem  22609  tgqioo  22650  re2ndc  22651  xrhmeo  22792  bndth  22804  pi1xfrcnvlem  22902  ovolficcss  23284  nulmbl2  23350  uniiccdif  23392  opnmbllem  23415  opnmblALT  23417  mbfimaopnlem  23467  i1fima  23490  i1fima2  23491  i1fd  23493  c1liplem1  23804  deg1n0ima  23894  efcvx  24248  dvrelog  24428  dvloglem  24439  logf1o2  24441  dvlog  24442  ressatans  24706  wilthlem3  24841  trkgbas  25389  trkgdist  25390  trkgitv  25391  ex-ss  27414  ajfval  27792  ipasslem8  27820  hlimcaui  28221  shsspwh  28231  hhssabloi  28247  hhssnv  28249  hhshsslem1  28252  shunssji  28356  sshhococi  28533  pjoml6i  28576  osumcori  28630  mayete3i  28715  mayetes3i  28716  imaelshi  29045  pjclem1  29182  pjci  29187  mdcompli  29416  dmdcompli  29417  xppreima  29577  gsummpt2co  29908  circtopn  30032  esumpcvgval  30268  esumcvg  30276  ldgenpisyslem3  30356  elmbfmvol2  30457  sxbrsigalem0  30461  eulerpartlemsv3  30551  ballotlem7  30725  rpsqrtcn  30799  bnj931  30967  bnj1137  31189  subfacp1lem2a  31288  subfacp1lem2b  31289  erdszelem2  31300  kur14lem7  31320  kur14lem9  31322  dfon2lem2  31813  bj-snglsstag  33094  bj-2upln1upl  33137  bj-0int  33180  bj-ccssccbar  33234  bj-ccinftyssccbar  33235  icoreelrn  33339  finxpreclem3  33360  imadifss  33514  poimirlem4  33543  poimirlem26  33565  poimirlem27  33566  opnmbllem0  33575  mblfinlem3  33578  mblfinlem4  33579  ismblfin  33580  volsupnfl  33584  sdclem2  33668  heibor1lem  33738  inxpssres  34217  dicval  36782  dvhdimlem  37050  ismrc  37581  mapfzcons1cl  37598  2rexfrabdioph  37677  3rexfrabdioph  37678  4rexfrabdioph  37679  6rexfrabdioph  37680  7rexfrabdioph  37681  rabdiophlem2  37683  jm2.27dlem5  37897  algbase  38065  algaddg  38066  algmulr  38067  algsca  38068  algvsca  38069  intimass2  38264  comptiunov2i  38315  relexp0a  38325  lhe4.4ex1a  38845  iocnct  40085  iccnct  40086  dvcosre  40444  fourierdlem46  40687  fourierdlem57  40698  fourierdlem58  40699  fourierdlem62  40703  fourierdlem102  40743  fourierdlem103  40744  fourierdlem104  40745  fourierdlem114  40755  sge0split  40944  sge0uzfsumgt  40979  hoiprodp1  41123  hoidmvlelem1  41130  hoidmvlelem2  41131  hoidmvlelem3  41132  sbgoldbo  42000  dmmpt2ssx2  42440  aacllem  42875
  Copyright terms: Public domain W3C validator