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

Theorem 3sstr4g 3219
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 3204 . 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 1623    C_ wss 3152
This theorem is referenced by:  rabss2  3256  unss2  3346  sslin  3395  ssopab2  4290  xpss12  4792  coss1  4839  coss2  4840  cnvss  4854  rnss  4907  ssres  4981  ssres2  4982  imass1  5048  imass2  5049  ssoprab2  5904  suppssfv  6074  suppssov1  6075  tposss  6235  onovuni  6359  ss2ixp  6829  fodomfi  7135  cantnfp1lem3  7382  isumsplit  12299  isumrpcl  12302  cvgrat  12339  gsumzf1o  15196  gsumzmhm  15210  gsumzinv  15217  divstgpopn  17802  metnrmlem2  18364  ovolsslem  18843  uniioombllem3  18940  ulmres  19767  xrlimcnp  20263  pntlemq  20750  subgornss  20973  sspba  21303  shlej2i  21958  chpssati  22943  subfacp1lem6  23716  predpredss  24172  ssoprab2g  25032  rnintintrn  25126  obsubc2  25850  idsubc  25851  domsubc  25852  codsubc  25853  morsubc  25855  cmpsubc  25856  aomclem4  27154  dsmmsubg  27209  bnj1408  29066
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator