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

Theorem sseqtr4i 3211
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 4-Apr-1995.)
Hypotheses
Ref Expression
sseqtr4.1  |-  A  C_  B
sseqtr4.2  |-  C  =  B
Assertion
Ref Expression
sseqtr4i  |-  A  C_  C

Proof of Theorem sseqtr4i
StepHypRef Expression
1 sseqtr4.1 . 2  |-  A  C_  B
2 sseqtr4.2 . . 3  |-  C  =  B
32eqcomi 2287 . 2  |-  B  =  C
41, 3sseqtri 3210 1  |-  A  C_  C
Colors of variables: wff set class
Syntax hints:    = wceq 1623    C_ wss 3152
This theorem is referenced by:  eqimss2i  3233  snsspr1  3764  snsspr2  3765  snsstp1  3766  snsstp2  3767  snsstp3  3768  unissint  3886  iunxdif2  3950  intabs  4172  sssucid  4469  opabssxp  4762  dmresi  5005  cnvimass  5033  ssrnres  5116  sofld  5121  cnvcnv  5126  cnvssrndm  5194  fvclss  5760  dmmpt2ssx  6189  tfrlem11  6404  oawordeulem  6552  mapex  6778  trcl  7410  dfac3  7748  cfsuc  7883  fin23lem11  7943  domtriomlem  8068  ttukeylem1  8136  ttukeylem7  8142  brdom7disj  8156  brdom6disj  8157  fingch  8245  fpwwe2lem13  8264  canthp1lem2  8275  wunex2  8360  wunex3  8363  ressxr  8876  ltrelxr  8886  nnssnn0  9968  un0addcl  9997  un0mulcl  9998  caubnd  11842  isumclim3  12222  znnen  12491  isprm3  12767  phimullem  12847  vdwnnlem1  13042  isstruct2  13157  2strbas  13245  2strop  13246  rngbase  13256  rngplusg  13257  rngmulr  13258  srngbase  13264  srngplusg  13265  srngmulr  13266  srnginvl  13267  lmodbase  13273  lmodplusg  13274  lmodsca  13275  lmodvsca  13276  algbase  13278  algaddg  13279  algmulr  13280  algsca  13281  algvsca  13282  phlbase  13288  phlplusg  13289  phlsca  13290  phlvsca  13291  phlip  13292  topgrpbas  13296  topgrpplusg  13297  topgrptset  13298  otpsbas  13303  otpstset  13304  otpsle  13305  odrngbas  13312  odrngplusg  13313  odrngmulr  13314  odrngtset  13315  odrngle  13316  odrngds  13317  homarw  13878  ipoval  14257  ipolerval  14259  cycsubg  14645  eqgfval  14665  gsumval3  15191  gsumzaddlem  15203  islbs3  15908  cnfldbas  16383  cnfldadd  16384  cnfldmul  16385  cnfldcj  16386  cnfldtset  16387  cnfldle  16388  cnfldds  16389  basdif0  16691  tgdif0  16730  iscldtop  16832  iocpnfordt  16945  icomnfordt  16946  iooordt  16947  cnrest2  17014  cmpcov2  17117  fiuncmp  17131  indiscon  17144  xkococnlem  17353  hmphdis  17487  uzrest  17592  ufildr  17626  fin1aufil  17627  eltsms  17815  qtopbaslem  18267  tgqioo  18306  re2ndc  18307  xrhmeo  18444  bndth  18456  pi1xfrcnvlem  18554  ovolficcss  18829  nulmbl2  18894  uniiccdif  18933  opnmbllem  18956  opnmblALT  18958  mbfimaopnlem  19010  i1fima  19033  i1fima2  19034  i1fd  19036  c1liplem1  19343  deg1n0ima  19475  efcvx  19825  dvrelog  19984  dvloglem  19995  logf1o2  19997  dvlog  19998  ressatans  20230  wilthlem3  20308  ex-ss  20814  ajfval  21387  ipasslem8  21415  hlimcaui  21816  shsspwh  21825  hhssabloi  21839  hhssnv  21841  hhshsslem1  21844  shunssji  21948  sshhococi  22125  pjoml6i  22168  osumcori  22222  mayete3i  22307  mayete3iOLD  22308  mayetes3i  22309  imaelshi  22638  pjclem1  22775  pjci  22780  mdcompli  23009  dmdcompli  23010  ballotlemsup  23063  ballotlem7  23094  xppreima  23211  fzssnn  23276  rnlogblem  23401  esumpcvgval  23446  esumcvg  23454  elmbfmvol2  23572  subfacp1lem2a  23711  subfacp1lem2b  23712  erdszelem2  23723  kur14lem7  23743  kur14lem9  23745  dfon2lem2  24140  wfrlem14  24269  bpoly4  24794  residcp  25077  imfstnrelc  25081  pvp  26048  pgapspf  26052  locfincmp  26304  sdclem2  26452  heibor1lem  26533  ismrc  26776  mapfzcons1cl  26795  2rexfrabdioph  26877  3rexfrabdioph  26878  4rexfrabdioph  26879  6rexfrabdioph  26880  7rexfrabdioph  26881  rabdiophlem2  26883  jm2.27dlem5  27106  lhe4.4ex1a  27546  dvcosre  27741  bnj931  28802  bnj1137  29025  dicval  31366  dvhdimlem  31634
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator