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

Theorem 3sstr4g 3609
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 3594 . 2 (𝐶𝐷𝐴𝐵)
51, 4sylibr 223 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  wss 3540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554
This theorem is referenced by:  rabss2  3648  unss2  3746  sslin  3801  intss  4433  ssopab2  4926  xpss12  5148  coss1  5199  coss2  5200  cnvss  5216  cnvssOLD  5217  rnss  5275  ssres  5344  ssres2  5345  imass1  5419  imass2  5420  predpredss  5603  ssoprab2  6609  ressuppss  7201  tposss  7240  onovuni  7326  ss2ixp  7807  fodomfi  8124  coss12d  13559  isumsplit  14411  isumrpcl  14414  cvgrat  14454  gsumzf1o  18136  gsumzmhm  18160  gsumzinv  18168  dsmmsubg  19906  qustgpopn  21733  metnrmlem2  22471  ovolsslem  23059  uniioombllem3  23159  ulmres  23946  xrlimcnp  24495  pntlemq  25090  sspba  26966  shlej2i  27622  chpssati  28606  mptssALT  28857  bnj1408  30358  subfacp1lem6  30421  mthmpps  30733  aomclem4  36645  cotrclrcl  37053  cusgredg  40646  fldc  41875  fldcALTV  41894
  Copyright terms: Public domain W3C validator