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

Theorem 3sstr4g 3232
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  |-  ( ph  ->  A  C_  B )
3sstr4g.2  |-  C  =  A
3sstr4g.3  |-  D  =  B
Assertion
Ref Expression
3sstr4g  |-  ( ph  ->  C  C_  D )

Proof of Theorem 3sstr4g
StepHypRef Expression
1 3sstr4g.1 . 2  |-  ( ph  ->  A  C_  B )
2 3sstr4g.2 . . 3  |-  C  =  A
3 3sstr4g.3 . . 3  |-  D  =  B
42, 3sseq12i 3217 . 2  |-  ( C 
C_  D  <->  A  C_  B
)
51, 4sylibr 203 1  |-  ( ph  ->  C  C_  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    C_ wss 3165
This theorem is referenced by:  rabss2  3269  unss2  3359  sslin  3408  ssopab2  4306  xpss12  4808  coss1  4855  coss2  4856  cnvss  4870  rnss  4923  ssres  4997  ssres2  4998  imass1  5064  imass2  5065  ssoprab2  5920  suppssfv  6090  suppssov1  6091  tposss  6251  onovuni  6375  ss2ixp  6845  fodomfi  7151  cantnfp1lem3  7398  isumsplit  12315  isumrpcl  12318  cvgrat  12355  gsumzf1o  15212  gsumzmhm  15226  gsumzinv  15233  divstgpopn  17818  metnrmlem2  18380  ovolsslem  18859  uniioombllem3  18956  ulmres  19783  xrlimcnp  20279  pntlemq  20766  subgornss  20989  sspba  21319  shlej2i  21974  chpssati  22959  subfacp1lem6  23731  predpredss  24243  ssoprab2g  25135  rnintintrn  25229  obsubc2  25953  idsubc  25954  domsubc  25955  codsubc  25956  morsubc  25958  cmpsubc  25959  aomclem4  27257  dsmmsubg  27312  bnj1408  29382
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator