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

Theorem 3sstr4g 4016
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 4001 . 2 (𝐶𝐷𝐴𝐵)
51, 4sylibr 235 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  wss 3940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-in 3947  df-ss 3956
This theorem is referenced by:  rabss2  4058  unss2  4161  sslin  4215  intss  4895  ssopab2  5430  xpss12  5569  coss1  5725  coss2  5726  cnvss  5742  rnss  5808  ssres  5879  ssres2  5880  imass1  5963  imass2  5964  predpredss  6153  ssoprab2  7216  ressuppss  7845  tposss  7889  onovuni  7975  ss2ixp  8468  fodomfi  8791  coss12d  14327  isumsplit  15190  isumrpcl  15193  cvgrat  15234  gsumzf1o  18968  gsumzmhm  18993  gsumzinv  19001  dsmmsubg  20822  qustgpopn  22662  metnrmlem2  23402  ovolsslem  24019  uniioombllem3  24120  ulmres  24910  xrlimcnp  25479  pntlemq  26110  cusgredg  27139  sspba  28437  shlej2i  29089  chpssati  30073  iunrnmptss  30251  mptssALT  30354  pmtrcnelor  30668  bnj1408  32211  subfacp1lem6  32335  mthmpps  32732  qsss1  35432  cossss  35556  aomclem4  39541  cotrclrcl  39971  symgsubmefmndALT  43970  fldc  44256  fldcALTV  44274
  Copyright terms: Public domain W3C validator