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

Theorem sseqtr4i 3498
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 2436 . 2  |-  B  =  C
41, 3sseqtri 3497 1  |-  A  C_  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1438    C_ wss 3437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-in 3444  df-ss 3451
This theorem is referenced by:  eqimss2i  3520  snsspr1  4147  snsspr2  4148  snsstp1  4149  snsstp2  4150  snsstp3  4151  unissint  4278  iunxdif2  4345  intabs  4583  opabssxp  4926  dmresi  5177  cnvimass  5205  ssrnres  5292  sofld  5301  cnvcnv  5305  cnvssrndm  5374  sssucid  5517  fvclss  6160  dmmpt2ssx  6870  suppun  6944  wfrlem14  7055  tfrlem11  7112  oawordeulem  7261  mapex  7484  trcl  8215  dfac3  8554  cfsuc  8689  fin23lem11  8749  domtriomlem  8874  ttukeylem1  8941  ttukeylem7  8947  brdom7disj  8961  brdom6disj  8962  fingch  9050  fpwwe2lem13  9069  canthp1lem2  9080  wunex2  9165  wunex3  9168  ressxr  9686  ltrelxr  9697  nnssnn0  10874  un0addcl  10905  un0mulcl  10906  fzssnn  11844  fzossnn0  11951  caubnd  13415  isumclim3  13813  iprodclim3  14046  bpoly4  14105  fprodefsum  14142  znnen  14258  isprm3  14626  phimullem  14720  vdwnnlem1  14938  isstruct2  15123  2strbas  15224  2strop  15225  2strbas1  15227  rngbase  15238  rngplusg  15239  rngmulr  15240  srngbase  15246  srngplusg  15247  srngmulr  15248  srnginvl  15249  lmodbase  15255  lmodplusg  15256  lmodsca  15257  lmodvsca  15258  ipsbase  15262  ipsaddg  15263  ipsmulr  15264  ipssca  15265  ipsvsca  15266  ipsip  15267  phlbase  15272  phlplusg  15273  phlsca  15274  phlvsca  15275  phlip  15276  topgrpbas  15280  topgrpplusg  15281  topgrptset  15282  otpsbas  15287  otpstset  15288  otpsle  15289  odrngbas  15298  odrngplusg  15299  odrngmulr  15300  odrngtset  15301  odrngle  15302  odrngds  15303  homarw  15934  ipoval  16393  ipolerval  16395  cycsubg  16838  eqgfval  16858  gsumval3  17534  nn0gsumfz  17606  islbs3  18371  cnfldbas  18967  cnfldadd  18968  cnfldmul  18969  cnfldcj  18970  cnfldtset  18971  cnfldle  18972  cnfldds  18973  cnfldunif  18974  pmatcollpw3fi  19801  basdif0  19960  iscldtop  20103  iocpnfordt  20223  icomnfordt  20224  iooordt  20225  cnrest2  20294  cmpcov2  20397  fiuncmp  20411  bwth  20417  indiscon  20425  locfincmp  20533  xkococnlem  20666  hmphdis  20803  uzrest  20904  ufildr  20938  fin1aufil  20939  eltsms  21139  ustval  21209  qtopbaslem  21771  tgqioo  21810  re2ndc  21811  xrhmeo  21966  bndth  21978  pi1xfrcnvlem  22079  ovolficcss  22414  nulmbl2  22482  uniiccdif  22527  opnmbllem  22551  opnmblALT  22553  mbfimaopnlem  22603  i1fima  22628  i1fima2  22629  i1fd  22631  c1liplem1  22940  deg1n0ima  23030  efcvx  23396  dvrelog  23574  dvloglem  23585  logf1o2  23587  dvlog  23588  ressatans  23852  wilthlem3  23987  trkgbas  24485  trkgdist  24486  trkgitv  24487  ex-ss  25869  ajfval  26442  ipasslem8  26470  hlimcaui  26881  shsspwh  26891  hhssabloi  26905  hhssnv  26907  hhshsslem1  26910  shunssji  27014  sshhococi  27191  pjoml6i  27234  osumcori  27288  mayete3i  27373  mayetes3i  27374  imaelshi  27703  pjclem1  27840  pjci  27845  mdcompli  28074  dmdcompli  28075  xppreima  28244  gsummpt2co  28544  circtopn  28666  esumpcvgval  28901  esumcvg  28909  ldgenpisyslem3  28989  elmbfmvol2  29091  sxbrsigalem0  29095  eulerpartlemsv3  29196  ballotlem7  29370  ballotlemsupOLD  29377  ballotlem7OLD  29408  bnj931  29584  bnj1137  29806  subfacp1lem2a  29905  subfacp1lem2b  29906  erdszelem2  29917  kur14lem7  29937  kur14lem9  29939  dfon2lem2  30431  bj-snglsstag  31537  bj-2upln1upl  31580  bj-ccssccbar  31617  bj-ccinftyssccbar  31618  icoreelrn  31711  imadifss  31848  poimirlem4  31864  poimirlem26  31886  poimirlem27  31887  opnmbllem0  31896  mblfinlem3  31899  mblfinlem4  31900  ismblfin  31901  volsupnfl  31905  sdclem2  31991  heibor1lem  32061  dicval  34669  dvhdimlem  34937  ismrc  35468  mapfzcons1cl  35485  2rexfrabdioph  35564  3rexfrabdioph  35565  4rexfrabdioph  35566  6rexfrabdioph  35567  7rexfrabdioph  35568  rabdiophlem2  35570  jm2.27dlem5  35794  algbase  35970  algaddg  35971  algmulr  35972  algsca  35973  algvsca  35974  intimass2  36113  comptiunov2i  36164  relexp0a  36174  lhe4.4ex1a  36542  dvcosre  37607  fourierdlem46  37842  fourierdlem57  37853  fourierdlem58  37854  fourierdlem62  37858  fourierdlem102  37898  fourierdlem103  37899  fourierdlem104  37900  fourierdlem114  37910  sge0split  38045  dmmpt2ssx2  39424  aacllem  39846
  Copyright terms: Public domain W3C validator