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

Theorem eqsstri 3284
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 3278 . 2  |-  ( A 
C_  C  <->  B  C_  C
)
41, 3mpbir 200 1  |-  A  C_  C
Colors of variables: wff set class
Syntax hints:    = wceq 1642    C_ wss 3228
This theorem is referenced by:  eqsstr3i  3285  ssrab2  3334  rabssab  3335  opabss  4159  epse  4455  omsson  4739  brab2ga  4842  relopabi  4890  dmopabss  4969  resss  5058  relres  5062  exse2  5126  rnin  5169  rnxpss  5187  cnvcnvss  5207  dmmptss  5248  fnres  5439  fabexg  5502  f0  5505  nfvres  5637  fvopab4ndm  5700  ffvresb  5770  funiunfv  5858  isoini2  5920  ovssunirn  5968  dmoprabss  6013  elmpt2cl  6145  frxp  6309  tposssxp  6322  dftpos4  6337  smores  6453  smores2  6455  iordsmo  6458  oawordeulem  6636  swoer  6772  swoord1  6773  swoord2  6774  ecss  6785  ecopovsym  6845  ecopovtrn  6846  ecopover  6847  sbthlem7  7062  nnfi  7138  imafi  7235  elfiun  7270  marypha1lem  7273  marypha2lem1  7275  ordtypelem2  7321  hartogslem1  7344  wemapso2  7354  wdomima2g  7387  inf3lem1  7416  cantnfres  7466  wemapwe  7487  tc2  7514  tz9.12lem1  7546  rankuni  7622  rankuniss  7625  cplem1  7646  hta  7654  r0weon  7727  infxpenlem  7728  ackbij1lem9  7941  ackbij1lem10  7942  ackbij1b  7952  cofsmo  7982  sdom2en01  8015  fin23lem26  8038  fin23lem28  8053  fin23lem30  8055  isf32lem5  8070  isf32lem6  8071  isf32lem7  8072  isf32lem8  8073  fin56  8106  fin1a2lem9  8121  hsmexlem4  8142  hsmexlem5  8143  hsmexlem6  8144  axdc3lem  8163  axdc3lem2  8164  axcclem  8170  zorn2lem1  8210  zorn2lem3  8212  zorn2lem4  8213  zorn2lem5  8214  imadomg  8246  iundom2g  8249  smobeth  8295  canth4  8356  gruina  8527  grur1a  8528  pinn  8589  niex  8592  ltsopi  8599  ltrelpi  8600  dmaddpi  8601  dmmulpi  8602  enqex  8633  0nnq  8635  elpqn  8636  ltrelnq  8637  nqerf  8641  nqerrel  8643  dmrecnq  8679  lterpq  8681  ltrelpr  8709  enrex  8779  ltrelsr  8780  dmaddsr  8794  dmmulsr  8795  ltrelre  8843  axaddf  8854  axmulf  8855  ltrelxr  8973  lerelxr  8975  nn0ssre  10058  nn0ssz  10133  uzsupss  10399  rpnnen1lem1  10431  rpnnen1lem2  10432  rpnnen1lem3  10433  rpnnen1lem5  10435  rpre  10449  uzsup  11056  fzfi  11123  swrd00  11541  sqrlem3  11820  sqrlem5  11822  cau3  11929  caubnd  11932  limsupgre  12045  rlimpm  12064  rlimclim  12110  isercolllem1  12228  isercolllem2  12229  isercoll  12231  caurcvg  12240  caucvg  12242  iseraltlem2  12246  iseraltlem3  12247  zsum  12282  fsumcvg3  12293  climfsum  12369  ackbijnn  12377  infcvgaux1i  12406  dvdszrcl  12627  divalglem2  12685  divalglem5  12687  divalglem8  12690  gcdcllem3  12783  bezoutlem2  12809  bezoutlem3  12810  maxprmfct  12883  phimullem  12938  eulerthlem2  12941  prmdiveq  12945  prmdivdiv  12946  pclem  12982  infpn2  13051  prmreclem2  13055  prmreclem3  13056  prmreclem5  13058  4sqlem1  13086  4sqlem13  13095  4sqlem14  13096  4sqlem17  13099  4sqlem18  13100  4sqlem19  13101  vdwnnlem3  13135  ramcl2lem  13147  ramtcl  13148  ramtcl2  13149  ramtub  13150  ramub1lem2  13165  structcnvcnv  13250  strlemor0  13325  strlemor1  13326  strleun  13329  prdsval  13448  prdsplusg  13451  prdsmulr  13452  prdsvsca  13453  prdshom  13459  imasdsval2  13512  gsumval1  14549  nmzsubg  14751  nmznsg  14754  conjnmz  14809  conjnmzb  14810  gicer  14833  gastacl  14856  sylow1lem2  15003  sylow1lem3  15004  sylow1lem4  15005  sylow1lem5  15006  sylow2a  15023  sylow3lem2  15032  efglem  15118  efgtf  15124  efgtlen  15128  efginvrel2  15129  efginvrel1  15130  efgsfo  15141  efgredlemg  15144  efgredleme  15145  efgredlemd  15146  efgredlemc  15147  efgredlem  15149  efgred  15150  efgrelexlemb  15152  efgcpbllemb  15157  frgpinv  15166  frgpuplem  15174  frgpupf  15175  frgpup1  15177  frgpnabllem2  15255  gsumval3  15284  ablfacrplem  15393  ablfacrp2  15395  ablfac1eu  15401  pgpfaclem1  15409  ablfaclem2  15414  ablfaclem3  15415  lspsolvlem  15988  lbsextlem2  16005  lbsextlem3  16006  lbsextlem4  16007  rrgeq0  16124  rrgss  16126  psrbagconf1o  16213  psrass1lem  16216  mplbasss  16270  ply1bascl  16377  coe1mul2lem2  16438  znf1o  16605  zntoslem  16610  cygznlem2a  16621  pjpm  16708  mretopd  16929  ordtbas  17022  leordtval2  17042  lecldbas  17049  lmfval  17062  lmbrf  17090  cnconst2  17111  hauscmplem  17233  concompcld  17260  hauspwdom  17327  txuni2  17360  xkouni  17394  xkoccn  17413  txkgen  17446  qtoptop2  17490  kqdisj  17523  hmphtop  17569  hmpher  17575  uzrest  17688  uzfbas  17689  lmflf  17796  ptcmplem1  17842  ptcmplem3  17844  tgpconcompeqg  17890  tgpconcomp  17891  imasdsf1olem  18033  xmeter  18075  blcld  18147  isngp2  18215  xrtgioo  18408  iccntr  18423  icccmplem1  18424  icccmplem2  18425  icccmplem3  18426  xmetdcn  18440  metdcn  18442  metdscn2  18458  icchmeo  18537  cnheiborlem  18550  lmmbrf  18786  iscau4  18803  iscauf  18804  caucfil  18807  lmclimf  18827  ivthlem1  18909  ivthlem2  18910  ivthlem3  18911  ovolsslem  18941  ovolicc2lem3  18976  ovolicc2lem4  18977  ovolicc2lem5  18978  ovolicc2  18979  volf  18986  uniioombllem3  19038  uniioombllem4  19039  uniioombllem5  19040  dyadmbllem  19052  dyadmbl  19053  volcn  19059  mbfimaopnlem  19108  mbflimsup  19119  i1f1  19143  itg2lcl  19180  iblmbf  19220  itgioo  19268  itgsplitioo  19290  limcflflem  19328  limcflf  19329  limcresi  19333  lhop  19461  dvfsumlem1  19471  dvfsumlem2  19472  dvfsumlem3  19473  dvfsumlem4  19474  dvfsumrlimge0  19475  dvfsumrlim  19476  dvfsumrlim2  19477  dvfsum2  19479  vieta1lem1  19788  vieta1lem2  19789  psercnlem2  19901  psercnlem1  19902  psercn  19903  pserdvlem1  19904  pserdvlem2  19905  pserdv  19906  pserdv2  19907  abelthlem4  19911  abelthlem6  19913  abelthlem9  19917  abelth  19918  logcnlem5  20098  dvlog  20103  dvlog2lem  20104  dvlog2  20105  cxpcn3lem  20192  cxpcn3  20193  sqrcn  20195  1cubr  20243  atansssdm  20334  atancn  20337  jensen  20388  wilthlem1  20412  ftalem3  20418  dvdsflip  20528  musum  20537  dvdsmulf1o  20540  fsumdvdsmul  20541  ppiub  20549  lgsfcl2  20647  lgseisenlem3  20696  lgseisenlem4  20697  lgsquadlem1  20699  lgsquadlem2  20700  lgsquadlem3  20701  2sqlem7  20715  rpvmasum2  20767  dchrisum0re  20768  dchrisum0lema  20769  dchrisum0lem1b  20770  dchrisum0lem1  20771  dchrisum0lem2a  20772  dchrisum0lem2  20773  dchrisum0lem3  20774  dchrisum0  20775  pntlem3  20864  issubgoi  21083  flddivrng  21188  phnv  21500  htthlem  21605  hlimadd  21880  hlimcaui  21924  hhsscms  21964  occllem  21990  shjshsi  22179  3oalem4  22352  pjfi  22391  dmadjss  22575  nlelshi  22748  nlelchi  22749  hmopidmchi  22839  atssch  23031  shatomistici  23049  mptctf  23313  cnre2csqima  23465  raddcn  23471  ustn0  23524  esumsn  23722  sxbrsiga  23904  ballotlemoex  23992  ballotlemfmpn  24001  ballotth  24044  lgamucov  24071  lgamucov2  24072  subfacp1lem3  24117  subfacp1lem5  24119  erdszelem2  24127  kur14lem3  24143  kur14lem6  24146  kur14lem7  24147  kur14lem9  24149  cvmlift2lem12  24249  ghomgrpilem2  24397  divcnvshft  24512  clim2prod  24517  ntrivcvg  24526  ntrivcvgfvn0  24528  ntrivcvgtail  24529  ntrivcvgmullem  24530  ntrivcvgmul  24531  zprod  24564  dfpo2  24670  predss  24731  wfrlem7  24820  frrlem7  24849  txpss3v  24976  pprodss4v  24982  relsset  24986  fixssdm  25004  fixssrn  25005  funpartss  25041  axcontlem2  25152  axcontlem7  25157  axcontlem8  25158  axcontlem10  25160  colinearex  25242  areacirc  25523  fneer  25612  neibastop1  25632  neibastop2lem  25633  filnetlem2  25652  filnetlem3  25653  caures  25800  bnd2lem  25838  ismtyres  25855  eldiophb  26159  rencldnfilem  26226  monotuz  26349  fglmod  26494  pwssplit4  26514  dsmmbase  26524  frlmsslsp  26571  pwfi2f1o  26583  mvdco  26711  symgsssg  26731  psgnghm  26760  rabexgf  27018  stoweidlem26  27098  stoweidlem44  27116  stoweidlem50  27122  stoweidlem51  27123  stoweidlem52  27124  stoweidlem57  27129  stoweidlem59  27131  mpt2ndm0  27442  nbgraf1olem1  27597  frgrawopreg1  27866  frgrawopreg2  27867  bnj21  28488  bnj1146  28568  bnj1292  28593  bnj1293  28594  bnj1145  28768  bnj1177  28781  toycom  29214  dihglblem2N  31536  lcdvbase  31835  mapdunirnN  31892
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-in 3235  df-ss 3242
  Copyright terms: Public domain W3C validator