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

Theorem 3sstr4g 3625
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 3610 . 2 (𝐶𝐷𝐴𝐵)
51, 4sylibr 224 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  wss 3555
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-in 3562  df-ss 3569
This theorem is referenced by:  rabss2  3664  unss2  3762  sslin  3817  intss  4463  ssopab2  4961  xpss12  5186  coss1  5237  coss2  5238  cnvss  5254  cnvssOLD  5255  rnss  5314  ssres  5383  ssres2  5384  imass1  5459  imass2  5460  predpredss  5645  ssoprab2  6664  ressuppss  7259  tposss  7298  onovuni  7384  ss2ixp  7865  fodomfi  8183  coss12d  13645  isumsplit  14497  isumrpcl  14500  cvgrat  14540  gsumzf1o  18234  gsumzmhm  18258  gsumzinv  18266  dsmmsubg  20006  qustgpopn  21833  metnrmlem2  22571  ovolsslem  23159  uniioombllem3  23259  ulmres  24046  xrlimcnp  24595  pntlemq  25190  cusgredg  26207  sspba  27428  shlej2i  28084  chpssati  29068  mptssALT  29314  bnj1408  30809  subfacp1lem6  30872  mthmpps  31184  aomclem4  37104  cotrclrcl  37512  fldc  41368  fldcALTV  41386
  Copyright terms: Public domain W3C validator