New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  eqsstri GIF version

Theorem eqsstri 3301
 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
Assertion
Ref Expression
eqsstri A C

Proof of Theorem eqsstri
StepHypRef Expression
1 eqsstr.2 . 2 B C
2 eqsstr.1 . . 3 A = B
32sseq1i 3295 . 2 (A CB C)
41, 3mpbir 200 1 A C
 Colors of variables: wff setvar class Syntax hints:   = wceq 1642   ⊆ wss 3257 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 1925  ax-ext 2334 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-v 2861  df-nin 3211  df-compl 3212  df-in 3213  df-ss 3259 This theorem is referenced by:  eqsstr3i  3302  ssrab2  3351  rabssab  3352  difsscompl  3549  pw1ss1c  4158  pw1sspw  4171  opkabssvvki  4209  imagekrelk  4273  dmopabss  4916  resss  4988  rnin  5037  rnxpss  5053  fun0  5154  fnres  5199  f0  5248  fvopab4ndm  5390  ffvresb  5431  isoini2  5498  dmoprabss  5575  dmmptss  5685  ecss  5966  nenpw1pwlem2  6085  sbthlem1  6203  spacssnc  6284  frecxp  6314
 Copyright terms: Public domain W3C validator