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

Theorem 3sstr4g 3795
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 3780 . 2 (𝐶𝐷𝐴𝐵)
51, 4sylibr 224 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1631  wss 3723
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-in 3730  df-ss 3737
This theorem is referenced by:  rabss2  3834  unss2  3935  sslin  3987  intss  4633  ssopab2  5135  xpss12  5265  coss1  5415  coss2  5416  cnvss  5432  rnss  5491  ssres  5564  ssres2  5565  imass1  5640  imass2  5641  predpredss  5828  ssoprab2  6862  ressuppss  7469  tposss  7509  onovuni  7596  ss2ixp  8079  fodomfi  8399  coss12d  13921  isumsplit  14779  isumrpcl  14782  cvgrat  14822  gsumzf1o  18520  gsumzmhm  18544  gsumzinv  18552  dsmmsubg  20304  qustgpopn  22143  metnrmlem2  22883  ovolsslem  23472  uniioombllem3  23573  ulmres  24362  xrlimcnp  24916  pntlemq  25511  cusgredg  26555  sspba  27922  shlej2i  28578  chpssati  29562  mptssALT  29814  bnj1408  31442  subfacp1lem6  31505  mthmpps  31817  qsss1  34394  cossss  34520  aomclem4  38151  cotrclrcl  38558  fldc  42606  fldcALTV  42624
  Copyright terms: Public domain W3C validator