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

Theorem 3sstr4g 4009
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 3994 . 2 (𝐶𝐷𝐴𝐵)
51, 4sylibr 235 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wss 3933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-in 3940  df-ss 3949
This theorem is referenced by:  rabss2  4051  unss2  4154  sslin  4208  intss  4888  ssopab2  5424  xpss12  5563  coss1  5719  coss2  5720  cnvss  5736  rnss  5802  ssres  5873  ssres2  5874  imass1  5957  imass2  5958  predpredss  6147  ssoprab2  7211  ressuppss  7838  tposss  7882  onovuni  7968  ss2ixp  8462  fodomfi  8785  coss12d  14320  isumsplit  15183  isumrpcl  15186  cvgrat  15227  gsumzf1o  18961  gsumzmhm  18986  gsumzinv  18994  dsmmsubg  20815  qustgpopn  22655  metnrmlem2  23395  ovolsslem  24012  uniioombllem3  24113  ulmres  24903  xrlimcnp  25473  pntlemq  26104  cusgredg  27133  sspba  28431  shlej2i  29083  chpssati  30067  iunrnmptss  30245  mptssALT  30348  pmtrcnelor  30662  bnj1408  32205  subfacp1lem6  32329  mthmpps  32726  qsss1  35426  cossss  35550  aomclem4  39535  cotrclrcl  39965  symgsubmefmndALT  43996  fldc  44282  fldcALTV  44300
  Copyright terms: Public domain W3C validator