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

Theorem sseqtr4i 3601
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 2619 . 2 𝐵 = 𝐶
41, 3sseqtri 3600 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1475  wss 3540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554
This theorem is referenced by:  eqimss2i  3623  snsspr1  4285  snsspr2  4286  snsstp1  4287  snsstp2  4288  snsstp3  4289  unissint  4436  iunxdif2  4504  intabs  4752  opabssxp  5116  dmresi  5376  cnvimass  5404  ssrnres  5491  sofld  5500  cnvcnv  5505  cnvssrndm  5574  sssucid  5719  fvclss  6404  dmmpt2ssx  7124  suppun  7202  wfrlem14  7315  tfrlem11  7371  oawordeulem  7521  mapex  7750  trcl  8487  dfac3  8827  cfsuc  8962  fin23lem11  9022  domtriomlem  9147  ttukeylem1  9214  ttukeylem7  9220  brdom7disj  9234  brdom6disj  9235  fingch  9324  fpwwe2lem13  9343  canthp1lem2  9354  wunex2  9439  wunex3  9442  ressxr  9962  ltrelxr  9978  nnssnn0  11172  un0addcl  11203  un0mulcl  11204  nn0ssxnn0  11243  fzssnn  12256  caubnd  13946  isumclim3  14332  iprodclim3  14570  bpoly4  14629  fprodefsum  14664  znnen  14780  isprm3  15234  phimullem  15322  vdwnnlem1  15537  isstruct2  15704  2strbas  15810  2strop  15811  2strbas1  15813  rngbase  15824  rngplusg  15825  rngmulr  15826  srngbase  15832  srngplusg  15833  srngmulr  15834  srnginvl  15835  lmodbase  15841  lmodplusg  15842  lmodsca  15843  lmodvsca  15844  ipsbase  15848  ipsaddg  15849  ipsmulr  15850  ipssca  15851  ipsvsca  15852  ipsip  15853  phlbase  15858  phlplusg  15859  phlsca  15860  phlvsca  15861  phlip  15862  topgrpbas  15866  topgrpplusg  15867  topgrptset  15868  otpsbas  15875  otpstset  15876  otpsle  15877  otpsbasOLD  15879  otpstsetOLD  15880  otpsleOLD  15881  odrngbas  15890  odrngplusg  15891  odrngmulr  15892  odrngtset  15893  odrngle  15894  odrngds  15895  homarw  16519  ipoval  16977  ipolerval  16979  cycsubg  17445  eqgfval  17465  gsumval3  18131  islbs3  18976  cnfldbas  19571  cnfldadd  19572  cnfldmul  19573  cnfldcj  19574  cnfldtset  19575  cnfldle  19576  cnfldds  19577  cnfldunif  19578  basdif0  20568  iscldtop  20709  iocpnfordt  20829  icomnfordt  20830  iooordt  20831  cnrest2  20900  cmpcov2  21003  fiuncmp  21017  bwth  21023  indiscon  21031  locfincmp  21139  xkococnlem  21272  hmphdis  21409  uzrest  21511  ufildr  21545  fin1aufil  21546  eltsms  21746  ustval  21816  qtopbaslem  22372  tgqioo  22411  re2ndc  22412  xrhmeo  22553  bndth  22565  pi1xfrcnvlem  22664  ovolficcss  23045  nulmbl2  23111  uniiccdif  23152  opnmbllem  23175  opnmblALT  23177  mbfimaopnlem  23228  i1fima  23251  i1fima2  23252  i1fd  23254  c1liplem1  23563  deg1n0ima  23653  efcvx  24007  dvrelog  24183  dvloglem  24194  logf1o2  24196  dvlog  24197  ressatans  24461  wilthlem3  24596  trkgbas  25144  trkgdist  25145  trkgitv  25146  ex-ss  26676  ajfval  27048  ipasslem8  27076  hlimcaui  27477  shsspwh  27487  hhssabloi  27503  hhssnv  27505  hhshsslem1  27508  shunssji  27612  sshhococi  27789  pjoml6i  27832  osumcori  27886  mayete3i  27971  mayetes3i  27972  imaelshi  28301  pjclem1  28438  pjci  28443  mdcompli  28672  dmdcompli  28673  xppreima  28829  gsummpt2co  29111  circtopn  29232  esumpcvgval  29467  esumcvg  29475  ldgenpisyslem3  29555  elmbfmvol2  29656  sxbrsigalem0  29660  eulerpartlemsv3  29750  ballotlem7  29924  bnj931  30095  bnj1137  30317  subfacp1lem2a  30416  subfacp1lem2b  30417  erdszelem2  30428  kur14lem7  30448  kur14lem9  30450  dfon2lem2  30933  bj-snglsstag  32162  bj-2upln1upl  32205  bj-ccssccbar  32281  bj-ccinftyssccbar  32282  icoreelrn  32385  finxpreclem3  32406  imadifss  32554  poimirlem4  32583  poimirlem26  32605  poimirlem27  32606  opnmbllem0  32615  mblfinlem3  32618  mblfinlem4  32619  ismblfin  32620  volsupnfl  32624  sdclem2  32708  heibor1lem  32778  dicval  35483  dvhdimlem  35751  ismrc  36282  mapfzcons1cl  36299  2rexfrabdioph  36378  3rexfrabdioph  36379  4rexfrabdioph  36380  6rexfrabdioph  36381  7rexfrabdioph  36382  rabdiophlem2  36384  jm2.27dlem5  36598  algbase  36767  algaddg  36768  algmulr  36769  algsca  36770  algvsca  36771  intimass2  36966  comptiunov2i  37017  relexp0a  37027  lhe4.4ex1a  37550  iocnct  38614  iccnct  38615  dvcosre  38799  fourierdlem46  39045  fourierdlem57  39056  fourierdlem58  39057  fourierdlem62  39061  fourierdlem102  39101  fourierdlem103  39102  fourierdlem104  39103  fourierdlem114  39113  sge0split  39302  sge0uzfsumgt  39337  hoiprodp1  39478  hoidmvlelem1  39485  hoidmvlelem2  39486  hoidmvlelem3  39487  dmmpt2ssx2  41908  aacllem  42356
  Copyright terms: Public domain W3C validator