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

Theorem sseqtr4i 3779
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 2769 . 2 𝐵 = 𝐶
41, 3sseqtri 3778 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1632  wss 3715
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-in 3722  df-ss 3729
This theorem is referenced by:  eqimss2i  3801  snsspr1  4490  snsspr2  4491  snsstp1  4492  snsstp2  4493  snsstp3  4494  unissint  4653  iunxdif2  4720  pwpwssunieq  4767  intabs  4974  opabssxp  5350  dmresi  5615  cnvimass  5643  ssrnres  5730  sofld  5739  cnvcnv  5744  cnvcnvOLD  5745  cnvssrndm  5818  sssucid  5963  fvclss  6663  dmmpt2ssx  7403  suppun  7483  wfrlem14  7597  tfrlem11  7653  oawordeulem  7803  mapex  8029  trcl  8777  dfac3  9134  cfsuc  9271  fin23lem11  9331  domtriomlem  9456  ttukeylem1  9523  ttukeylem7  9529  brdom7disj  9545  brdom6disj  9546  fingch  9637  fpwwe2lem13  9656  canthp1lem2  9667  wunex2  9752  wunex3  9755  ressxr  10275  ltrelxr  10291  nnssnn0  11487  un0addcl  11518  un0mulcl  11519  nn0ssxnn0  11558  fzssnn  12578  caubnd  14297  isumclim3  14689  iprodclim3  14930  bpoly4  14989  fprodefsum  15024  znnen  15140  isprm3  15598  phimullem  15686  vdwnnlem1  15901  isstruct2  16069  2strbas  16186  2strop  16187  2strbas1  16189  rngbase  16203  rngplusg  16204  rngmulr  16205  srngbase  16211  srngplusg  16212  srngmulr  16213  srnginvl  16214  lmodbase  16220  lmodplusg  16221  lmodsca  16222  lmodvsca  16223  ipsbase  16227  ipsaddg  16228  ipsmulr  16229  ipssca  16230  ipsvsca  16231  ipsip  16232  phlbase  16237  phlplusg  16238  phlsca  16239  phlvsca  16240  phlip  16241  topgrpbas  16245  topgrpplusg  16246  topgrptset  16247  otpsbas  16254  otpstset  16255  otpsle  16256  otpsbasOLD  16258  otpstsetOLD  16259  otpsleOLD  16260  odrngbas  16269  odrngplusg  16270  odrngmulr  16271  odrngtset  16272  odrngle  16273  odrngds  16274  homarw  16897  ipoval  17355  ipolerval  17357  cycsubg  17823  eqgfval  17843  gsumval3  18508  islbs3  19357  cnfldbas  19952  cnfldadd  19953  cnfldmul  19954  cnfldcj  19955  cnfldtset  19956  cnfldle  19957  cnfldds  19958  cnfldunif  19959  basdif0  20959  iscldtop  21101  iocpnfordt  21221  icomnfordt  21222  iooordt  21223  cnrest2  21292  cmpcov2  21395  fiuncmp  21409  bwth  21415  indisconn  21423  locfincmp  21531  xkococnlem  21664  hmphdis  21801  uzrest  21902  ufildr  21936  fin1aufil  21937  eltsms  22137  ustval  22207  qtopbaslem  22763  tgqioo  22804  re2ndc  22805  xrhmeo  22946  bndth  22958  pi1xfrcnvlem  23056  ovolficcss  23438  nulmbl2  23504  uniiccdif  23546  opnmbllem  23569  opnmblALT  23571  mbfimaopnlem  23621  i1fima  23644  i1fima2  23645  i1fd  23647  c1liplem1  23958  deg1n0ima  24048  efcvx  24402  dvrelog  24582  dvloglem  24593  logf1o2  24595  dvlog  24596  ressatans  24860  wilthlem3  24995  trkgbas  25543  trkgdist  25544  trkgitv  25545  ex-ss  27595  ajfval  27973  ipasslem8  28001  hlimcaui  28402  shsspwh  28412  hhssabloi  28428  hhssnv  28430  hhshsslem1  28433  shunssji  28537  sshhococi  28714  pjoml6i  28757  osumcori  28811  mayete3i  28896  mayetes3i  28897  imaelshi  29226  pjclem1  29363  pjci  29368  mdcompli  29597  dmdcompli  29598  xppreima  29758  gsummpt2co  30089  circtopn  30213  esumpcvgval  30449  esumcvg  30457  ldgenpisyslem3  30537  elmbfmvol2  30638  sxbrsigalem0  30642  eulerpartlemsv3  30732  ballotlem7  30906  rpsqrtcn  30980  bnj931  31148  bnj1137  31370  subfacp1lem2a  31469  subfacp1lem2b  31470  erdszelem2  31481  kur14lem7  31501  kur14lem9  31503  dfon2lem2  31994  bj-snglsstag  33275  bj-2upln1upl  33318  bj-0int  33361  bj-ccssccbar  33415  bj-ccinftyssccbar  33416  icoreelrn  33520  finxpreclem3  33541  imadifss  33697  poimirlem4  33726  poimirlem26  33748  poimirlem27  33749  opnmbllem0  33758  mblfinlem3  33761  mblfinlem4  33762  ismblfin  33763  volsupnfl  33767  sdclem2  33851  heibor1lem  33921  inxpssres  34400  dicval  36967  dvhdimlem  37235  ismrc  37766  mapfzcons1cl  37783  2rexfrabdioph  37862  3rexfrabdioph  37863  4rexfrabdioph  37864  6rexfrabdioph  37865  7rexfrabdioph  37866  rabdiophlem2  37868  jm2.27dlem5  38082  algbase  38250  algaddg  38251  algmulr  38252  algsca  38253  algvsca  38254  intimass2  38449  comptiunov2i  38500  relexp0a  38510  lhe4.4ex1a  39030  iocnct  40270  iccnct  40271  dvcosre  40629  fourierdlem46  40872  fourierdlem57  40883  fourierdlem58  40884  fourierdlem62  40888  fourierdlem102  40928  fourierdlem103  40929  fourierdlem104  40930  fourierdlem114  40940  sge0split  41129  sge0uzfsumgt  41164  hoiprodp1  41308  hoidmvlelem1  41315  hoidmvlelem2  41316  hoidmvlelem3  41317  sbgoldbo  42185  dmmpt2ssx2  42625  aacllem  43060
  Copyright terms: Public domain W3C validator