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

Theorem 3sstr4g 3806
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 3791 . 2 (𝐶𝐷𝐴𝐵)
51, 4sylibr 225 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1652  wss 3732
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-in 3739  df-ss 3746
This theorem is referenced by:  rabss2  3845  unss2  3946  sslin  3998  intss  4654  ssopab2  5162  xpss12  5292  coss1  5446  coss2  5447  cnvss  5463  rnss  5522  ssres  5599  ssres2  5600  imass1  5682  imass2  5683  predpredss  5871  ssoprab2  6909  ressuppss  7516  tposss  7556  onovuni  7643  ss2ixp  8126  fodomfi  8446  coss12d  14000  isumsplit  14858  isumrpcl  14861  cvgrat  14900  gsumzf1o  18579  gsumzmhm  18603  gsumzinv  18611  dsmmsubg  20363  qustgpopn  22202  metnrmlem2  22942  ovolsslem  23542  uniioombllem3  23643  ulmres  24433  xrlimcnp  24986  pntlemq  25581  cusgredg  26611  sspba  27973  shlej2i  28629  chpssati  29613  mptssALT  29858  bnj1408  31484  subfacp1lem6  31547  mthmpps  31859  qsss1  34417  cossss  34541  aomclem4  38236  cotrclrcl  38641  fldc  42684  fldcALTV  42702
  Copyright terms: Public domain W3C validator