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

Theorem 3sstr4g 3508
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 3493 . 2  |-  ( C 
C_  D  <->  A  C_  B
)
51, 4sylibr 212 1  |-  ( ph  ->  C  C_  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370    C_ wss 3439
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3446  df-ss 3453
This theorem is referenced by:  rabss2  3546  unss2  3638  sslin  3687  ssopab2  4725  xpss12  5056  coss1  5106  coss2  5107  cnvss  5123  rnss  5179  ssres  5247  ssres2  5248  imass1  5314  imass2  5315  ssoprab2  6254  suppssfvOLD  6429  suppssov1OLD  6430  ressuppss  6821  tposss  6859  onovuni  6916  ss2ixp  7389  fodomfi  7704  cantnfp1lem3OLD  8029  isumsplit  13425  isumrpcl  13428  cvgrat  13465  gsumzf1o  16516  gsumzf1oOLD  16519  gsumzmhm  16556  gsumzmhmOLD  16557  gsumzinv  16568  gsumzinvOLD  16569  dsmmsubg  18303  divstgpopn  19832  metnrmlem2  20578  ovolsslem  21109  uniioombllem3  21208  ulmres  21996  xrlimcnp  22505  pntlemq  22993  subgornss  23972  sspba  24304  shlej2i  24961  chpssati  25946  sitgclbn  26896  subfacp1lem6  27240  predpredss  27798  aomclem4  29581  scmatdmat  31085  bnj1408  32382
  Copyright terms: Public domain W3C validator