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

Theorem sseqtr4i 3536
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 2470 . 2
41, 3sseqtri 3535 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395  C_wss 3475
This theorem is referenced by:  eqimss2i  3558  snsspr1  4179  snsspr2  4180  snsstp1  4181  snsstp2  4182  snsstp3  4183  unissint  4311  iunxdif2  4378  intabs  4613  sssucid  4960  opabssxp  5079  dmresi  5334  cnvimass  5362  ssrnres  5450  sofld  5460  cnvcnv  5464  cnvssrndm  5534  fvclss  6154  dmmpt2ssx  6865  suppun  6939  tfrlem11  7076  oawordeulem  7222  mapex  7445  trcl  8180  dfac3  8523  cfsuc  8658  fin23lem11  8718  domtriomlem  8843  ttukeylem1  8910  ttukeylem7  8916  brdom7disj  8930  brdom6disj  8931  fingch  9022  fpwwe2lem13  9041  canthp1lem2  9052  wunex2  9137  wunex3  9140  ressxr  9658  ltrelxr  9669  nnssnn0  10823  un0addcl  10854  un0mulcl  10855  fzossnn0  11856  caubnd  13191  isumclim3  13574  iprodclim3  13793  fprodefsum  13830  znnen  13946  isprm3  14226  phimullem  14309  vdwnnlem1  14513  isstruct2  14641  2strbas  14734  2strop  14735  rngbase  14745  rngplusg  14746  rngmulr  14747  srngbase  14753  srngplusg  14754  srngmulr  14755  srnginvl  14756  lmodbase  14762  lmodplusg  14763  lmodsca  14764  lmodvsca  14765  ipsbase  14769  ipsaddg  14770  ipsmulr  14771  ipssca  14772  ipsvsca  14773  ipsip  14774  phlbase  14779  phlplusg  14780  phlsca  14781  phlvsca  14782  phlip  14783  topgrpbas  14787  topgrpplusg  14788  topgrptset  14789  otpsbas  14794  otpstset  14795  otpsle  14796  odrngbas  14805  odrngplusg  14806  odrngmulr  14807  odrngtset  14808  odrngle  14809  odrngds  14810  homarw  15373  ipoval  15784  ipolerval  15786  cycsubg  16229  eqgfval  16249  gsumval3OLD  16908  gsumval3  16911  gsumzaddlemOLD  16936  nn0gsumfz  17012  islbs3  17801  cnfldbas  18424  cnfldadd  18425  cnfldmul  18426  cnfldcj  18427  cnfldtset  18428  cnfldle  18429  cnfldds  18430  cnfldunif  18431  pmatcollpw3fi  19286  basdif0  19454  iscldtop  19596  iocpnfordt  19716  icomnfordt  19717  iooordt  19718  cnrest2  19787  cmpcov2  19890  fiuncmp  19904  bwth  19910  indiscon  19919  locfincmp  20027  xkococnlem  20160  hmphdis  20297  uzrest  20398  ufildr  20432  fin1aufil  20433  eltsms  20631  ustval  20705  qtopbaslem  21265  tgqioo  21305  re2ndc  21306  xrhmeo  21446  bndth  21458  pi1xfrcnvlem  21556  ovolficcss  21881  nulmbl2  21947  uniiccdif  21987  opnmbllem  22010  opnmblALT  22012  mbfimaopnlem  22062  i1fima  22085  i1fima2  22086  i1fd  22088  c1liplem1  22397  deg1n0ima  22489  efcvx  22844  dvrelog  23018  dvloglem  23029  logf1o2  23031  dvlog  23032  ressatans  23265  wilthlem3  23344  trkgbas  23841  trkgdist  23842  trkgitv  23843  ex-ss  25148  ajfval  25724  ipasslem8  25752  hlimcaui  26154  shsspwh  26164  hhssabloi  26178  hhssnv  26180  hhshsslem1  26183  shunssji  26287  sshhococi  26464  pjoml6i  26507  osumcori  26561  mayete3i  26646  mayete3iOLD  26647  mayetes3i  26648  imaelshi  26977  pjclem1  27114  pjci  27119  mdcompli  27348  dmdcompli  27349  xppreima  27487  fzssnn  27595  circtopn  27840  esumpcvgval  28084  esumcvg  28092  elmbfmvol2  28238  sxbrsigalem0  28242  eulerpartlemsv3  28300  ballotlemsup  28443  ballotlem7  28474  subfacp1lem2a  28624  subfacp1lem2b  28625  erdszelem2  28636  kur14lem7  28656  kur14lem9  28658  dfon2lem2  29216  wfrlem14  29356  bpoly4  29821  opnmbllem0  30050  mblfinlem3  30053  mblfinlem4  30054  ismblfin  30055  volsupnfl  30059  sdclem2  30235  heibor1lem  30305  ismrc  30633  mapfzcons1cl  30650  2rexfrabdioph  30729  3rexfrabdioph  30730  4rexfrabdioph  30731  6rexfrabdioph  30732  7rexfrabdioph  30733  rabdiophlem2  30735  jm2.27dlem5  30955  algbase  31127  algaddg  31128  algmulr  31129  algsca  31130  algvsca  31131  lhe4.4ex1a  31234  dvcosre  31706  fourierdlem46  31935  fourierdlem57  31946  fourierdlem58  31947  fourierdlem62  31951  fourierdlem102  31991  fourierdlem103  31992  fourierdlem104  31993  fourierdlem114  32003  dmmpt2ssx2  32926  aacllem  33216  bnj931  33829  bnj1137  34051  bj-snglsstag  34539  bj-2upln1upl  34582  bj-ccssccbar  34620  bj-ccinftyssccbar  34621  dicval  36903  dvhdimlem  37171  intimass2  37769
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489
  Copyright terms: Public domain W3C validator