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

Theorem eqsstri 3370
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 16-Jul-1995.)
Hypotheses
Ref Expression
eqsstr.1  |-  A  =  B
eqsstr.2  |-  B  C_  C
Assertion
Ref Expression
eqsstri  |-  A  C_  C

Proof of Theorem eqsstri
StepHypRef Expression
1 eqsstr.2 . 2  |-  B  C_  C
2 eqsstr.1 . . 3  |-  A  =  B
32sseq1i 3364 . 2  |-  ( A 
C_  C  <->  B  C_  C
)
41, 3mpbir 201 1  |-  A  C_  C
Colors of variables: wff set class
Syntax hints:    = wceq 1652    C_ wss 3312
This theorem is referenced by:  eqsstr3i  3371  ssrab2  3420  rabssab  3422  opabss  4261  omsson  4841  brab2ga  4943  relopabi  4992  dmopabss  5073  resss  5162  relres  5166  exse2  5230  rnin  5273  rnxpss  5293  cnvcnvss  5317  dmmptss  5358  fnres  5553  fabexg  5616  f0  5619  nfvres  5752  fvopab4ndm  5817  ffvresb  5892  funiunfv  5987  isoini2  6051  ovssunirn  6099  dmoprabss  6147  elmpt2cl  6280  frxp  6448  mpt2ndm0  6465  tposssxp  6475  dftpos4  6490  smores  6606  smores2  6608  iordsmo  6611  oawordeulem  6789  swoer  6925  swoord1  6926  swoord2  6927  ecss  6938  ecopovsym  6998  ecopovtrn  6999  ecopover  7000  sbthlem7  7215  nnfi  7291  imafi  7391  elfiun  7427  marypha1lem  7430  marypha2lem1  7432  ordtypelem2  7480  hartogslem1  7503  wemapso2  7513  wdomima2g  7546  inf3lem1  7575  cantnfres  7625  wemapwe  7646  tc2  7673  tz9.12lem1  7705  rankuni  7781  rankuniss  7784  cplem1  7805  hta  7813  r0weon  7886  infxpenlem  7887  ackbij1lem9  8100  ackbij1lem10  8101  ackbij1b  8111  cofsmo  8141  sdom2en01  8174  fin23lem26  8197  fin23lem28  8212  fin23lem30  8214  isf32lem5  8229  isf32lem6  8230  isf32lem7  8231  isf32lem8  8232  fin56  8265  fin1a2lem9  8280  hsmexlem4  8301  hsmexlem5  8302  hsmexlem6  8303  axdc3lem  8322  axdc3lem2  8323  axcclem  8329  zorn2lem1  8368  zorn2lem3  8370  zorn2lem4  8371  zorn2lem5  8372  imadomg  8404  iundom2g  8407  smobeth  8453  canth4  8514  gruina  8685  grur1a  8686  pinn  8747  niex  8750  ltsopi  8757  ltrelpi  8758  dmaddpi  8759  dmmulpi  8760  enqex  8791  0nnq  8793  elpqn  8794  ltrelnq  8795  nqerf  8799  nqerrel  8801  dmrecnq  8837  lterpq  8839  ltrelpr  8867  enrex  8937  ltrelsr  8938  dmaddsr  8952  dmmulsr  8953  ltrelre  9001  axaddf  9012  axmulf  9013  ltrelxr  9131  lerelxr  9133  nn0ssre  10217  nn0ssz  10294  uzsupss  10560  rpnnen1lem1  10592  rpnnen1lem2  10593  rpnnen1lem3  10594  rpnnen1lem5  10596  rpre  10610  uzsup  11236  fzfi  11303  swrd00  11757  sqrlem3  12042  sqrlem5  12044  cau3  12151  caubnd  12154  limsupgre  12267  rlimpm  12286  rlimclim  12332  isercolllem1  12450  isercolllem2  12451  isercoll  12453  caurcvg  12462  caucvg  12464  iseraltlem2  12468  iseraltlem3  12469  zsum  12504  fsumcvg3  12515  climfsum  12591  ackbijnn  12599  infcvgaux1i  12628  dvdszrcl  12849  divalglem2  12907  divalglem5  12909  divalglem8  12912  gcdcllem3  13005  bezoutlem2  13031  bezoutlem3  13032  maxprmfct  13105  phimullem  13160  eulerthlem2  13163  prmdiveq  13167  prmdivdiv  13168  pclem  13204  infpn2  13273  prmreclem2  13277  prmreclem3  13278  prmreclem5  13280  4sqlem1  13308  4sqlem13  13317  4sqlem14  13318  4sqlem17  13321  4sqlem18  13322  4sqlem19  13323  vdwnnlem3  13357  ramcl2lem  13369  ramtcl  13370  ramtcl2  13371  ramtub  13372  ramub1lem2  13387  structcnvcnv  13472  strlemor0  13547  strlemor1  13548  strleun  13551  imasdsval2  13734  gsumval1  14771  nmzsubg  14973  nmznsg  14976  conjnmz  15031  conjnmzb  15032  gicer  15055  gastacl  15078  sylow1lem2  15225  sylow1lem3  15226  sylow1lem4  15227  sylow1lem5  15228  sylow2a  15245  sylow3lem2  15254  efglem  15340  efgtf  15346  efgtlen  15350  efginvrel2  15351  efginvrel1  15352  efgsfo  15363  efgredlemg  15366  efgredleme  15367  efgredlemd  15368  efgredlemc  15369  efgredlem  15371  efgred  15372  efgrelexlemb  15374  efgcpbllemb  15379  frgpinv  15388  frgpuplem  15396  frgpupf  15397  frgpup1  15399  frgpnabllem2  15477  gsumval3  15506  ablfacrplem  15615  ablfacrp2  15617  ablfac1eu  15623  pgpfaclem1  15631  ablfaclem2  15636  ablfaclem3  15637  lspsolvlem  16206  lbsextlem2  16223  lbsextlem3  16224  lbsextlem4  16225  rrgeq0  16342  rrgss  16344  psrbagconf1o  16431  psrass1lem  16434  mplbasss  16488  ply1bascl  16593  coe1mul2lem2  16653  znf1o  16824  zntoslem  16829  cygznlem2a  16840  pjpm  16927  mretopd  17148  ordtbas  17248  leordtval2  17268  lecldbas  17275  lmfval  17288  lmbrf  17316  cnconst2  17339  hauscmplem  17461  concompcld  17489  hauspwdom  17556  txuni2  17589  xkouni  17623  xkoccn  17643  txkgen  17676  qtoptop2  17723  kqdisj  17756  hmphtop  17802  hmpher  17808  uzrest  17921  uzfbas  17922  lmflf  18029  ptcmplem1  18075  ptcmplem3  18077  tgpconcompeqg  18133  tgpconcomp  18134  ustn0  18242  imasdsf1olem  18395  xmeter  18455  blcld  18527  isngp2  18636  xrtgioo  18829  iccntr  18844  icccmplem1  18845  icccmplem2  18846  icccmplem3  18847  xmetdcn  18861  metdcn  18863  metdscn2  18879  icchmeo  18958  cnheiborlem  18971  lmmbrf  19207  iscau4  19224  iscauf  19225  caucfil  19228  lmclimf  19248  ivthlem1  19340  ivthlem2  19341  ivthlem3  19342  ovolsslem  19372  ovolicc2lem3  19407  ovolicc2lem4  19408  ovolicc2lem5  19409  ovolicc2  19410  volf  19417  uniioombllem3  19469  uniioombllem4  19470  uniioombllem5  19471  dyadmbllem  19483  dyadmbl  19484  volcn  19490  mbfimaopnlem  19539  mbflimsup  19550  i1f1  19574  itg2lcl  19611  iblmbf  19651  itgioo  19699  itgsplitioo  19721  limcflflem  19759  limcflf  19760  limcresi  19764  lhop  19892  dvfsumlem1  19902  dvfsumlem2  19903  dvfsumlem3  19904  dvfsumlem4  19905  dvfsumrlimge0  19906  dvfsumrlim  19907  dvfsumrlim2  19908  dvfsum2  19910  vieta1lem1  20219  vieta1lem2  20220  psercnlem2  20332  psercnlem1  20333  psercn  20334  pserdvlem1  20335  pserdvlem2  20336  pserdv  20337  pserdv2  20338  abelthlem4  20342  abelthlem6  20344  abelthlem9  20348  abelth  20349  logcnlem5  20529  dvlog  20534  dvlog2lem  20535  dvlog2  20536  cxpcn3lem  20623  cxpcn3  20624  sqrcn  20626  1cubr  20674  atansssdm  20765  atancn  20768  jensen  20819  wilthlem1  20843  ftalem3  20849  dvdsflip  20959  musum  20968  dvdsmulf1o  20971  fsumdvdsmul  20972  ppiub  20980  lgsfcl2  21078  lgseisenlem3  21127  lgseisenlem4  21128  lgsquadlem1  21130  lgsquadlem2  21131  lgsquadlem3  21132  2sqlem7  21146  rpvmasum2  21198  dchrisum0re  21199  dchrisum0lema  21200  dchrisum0lem1b  21201  dchrisum0lem1  21202  dchrisum0lem2a  21203  dchrisum0lem2  21204  dchrisum0lem3  21205  dchrisum0  21206  pntlem3  21295  nbgraf1olem1  21443  issubgoi  21890  flddivrng  21995  phnv  22307  htthlem  22412  hlimadd  22687  hlimcaui  22731  hhsscms  22771  occllem  22797  shjshsi  22986  3oalem4  23159  pjfi  23198  dmadjss  23382  nlelshi  23555  nlelchi  23556  hmopidmchi  23646  atssch  23838  shatomistici  23856  mptctf  24104  cnre2csqima  24301  raddcn  24307  rrhre  24379  esumsn  24448  sxbrsiga  24632  sitmcl  24655  ballotlemoex  24735  ballotlemfmpn  24744  ballotth  24787  lgamucov  24814  lgamucov2  24815  subfacp1lem3  24860  subfacp1lem5  24862  erdszelem2  24870  kur14lem3  24886  kur14lem6  24889  kur14lem7  24890  kur14lem9  24892  cvmlift2lem12  24993  ghomgrpilem2  25089  divcnvshft  25203  clim2prod  25208  ntrivcvg  25217  ntrivcvgfvn0  25219  ntrivcvgtail  25220  ntrivcvgmullem  25221  ntrivcvgmul  25222  zprod  25255  dfpo2  25370  predss  25438  wfrlem7  25536  wlimss  25572  frrlem7  25584  txpss3v  25715  pprodss4v  25721  relsset  25725  fixssdm  25743  fixssrn  25744  limitssson  25748  funpartss  25781  axcontlem2  25896  axcontlem7  25901  axcontlem8  25902  axcontlem10  25904  colinearex  25986  areacirc  26288  fneer  26359  neibastop1  26379  neibastop2lem  26380  filnetlem2  26399  filnetlem3  26400  caures  26457  bnd2lem  26491  ismtyres  26508  eldiophb  26806  monotuz  26995  fglmod  27139  pwssplit4  27159  dsmmbase  27169  frlmsslsp  27216  pwfi2f1o  27228  mvdco  27356  symgsssg  27376  psgnghm  27405  rabexgf  27662  stoweidlem26  27742  stoweidlem44  27760  stoweidlem50  27766  stoweidlem51  27767  stoweidlem52  27768  stoweidlem57  27773  stoweidlem59  27775  frgrawopreg1  28376  frgrawopreg2  28377  bnj21  29019  bnj1146  29099  bnj1292  29124  bnj1293  29125  bnj1145  29299  bnj1177  29312  toycom  29707  dihglblem2N  32029  lcdvbase  32328  mapdunirnN  32385
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator