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

Theorem 3sstr4g 3544
 Description: Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
Hypotheses
Ref Expression
3sstr4g.1
3sstr4g.2
3sstr4g.3
Assertion
Ref Expression
3sstr4g

Proof of Theorem 3sstr4g
StepHypRef Expression
1 3sstr4g.1 . 2
2 3sstr4g.2 . . 3
3 3sstr4g.3 . . 3
42, 3sseq12i 3529 . 2
51, 4sylibr 212 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  =wceq 1395  C_wss 3475 This theorem is referenced by:  rabss2  3582  unss2  3674  sslin  3723  intss  4307  ssopab2  4778  xpss12  5113  coss1  5163  coss2  5164  cnvss  5180  rnss  5236  ssres  5304  ssres2  5305  imass1  5376  imass2  5377  ssoprab2  6353  suppssfvOLD  6531  suppssov1OLD  6532  ressuppss  6938  tposss  6975  onovuni  7032  ss2ixp  7502  fodomfi  7819  cantnfp1lem3OLD  8146  isumsplit  13652  isumrpcl  13655  cvgrat  13692  gsumzf1o  16917  gsumzf1oOLD  16920  gsumzmhm  16957  gsumzmhmOLD  16958  gsumzinv  16969  gsumzinvOLD  16970  dsmmsubg  18774  qustgpopn  20618  metnrmlem2  21364  ovolsslem  21895  uniioombllem3  21994  ulmres  22783  xrlimcnp  23298  pntlemq  23786  subgornss  25308  sspba  25640  shlej2i  26297  chpssati  27282  subfacp1lem6  28629  mthmpps  28942  predpredss  29250  aomclem4  31003  fldc  32891  fldcOLD  32910  bnj1408  34092  coss12d  37759 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489
 Copyright terms: Public domain W3C validator