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

Theorem 3sstr4g 3511
 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 3496 . 2
51, 4sylibr 215 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wceq 1437   wss 3442 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407 This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-in 3449  df-ss 3456 This theorem is referenced by:  rabss2  3550  unss2  3643  sslin  3694  intss  4279  ssopab2  4747  xpss12  4960  coss1  5010  coss2  5011  cnvss  5027  rnss  5083  ssres  5150  ssres2  5151  imass1  5223  imass2  5224  predpredss  5405  ssoprab2  6361  ressuppss  6945  tposss  6982  onovuni  7069  ss2ixp  7543  fodomfi  7856  coss12d  13015  isumsplit  13876  isumrpcl  13879  cvgrat  13917  gsumzf1o  17485  gsumzmhm  17509  gsumzinv  17517  dsmmsubg  19241  qustgpopn  21069  metnrmlem2  21792  ovolsslem  22322  uniioombllem3  22428  ulmres  23216  xrlimcnp  23767  pntlemq  24310  subgornss  25887  sspba  26219  shlej2i  26875  chpssati  27859  fmptss  28125  bnj1408  29641  subfacp1lem6  29704  mthmpps  30016  aomclem4  35636  cotrclrcl  35988  fldc  38867  fldcALTV  38886
 Copyright terms: Public domain W3C validator