ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sstr2 Structured version   Unicode version

Theorem sstr2 2946
Description: Transitivity of subclasses. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
Assertion
Ref Expression
sstr2 
C_  C_  C  C_  C

Proof of Theorem sstr2
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 ssel 2933 . . . 4 
C_
21imim1d 69 . . 3 
C_  C  C
32alimdv 1756 . 2 
C_  C  C
4 dfss2 2928 . 2 
C_  C  C
5 dfss2 2928 . 2 
C_  C  C
63, 4, 53imtr4g 194 1 
C_  C_  C  C_  C
Colors of variables: wff set class
Syntax hints:   wi 4  wal 1240   wcel 1390    C_ wss 2911
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-11 1394  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-in 2918  df-ss 2925
This theorem is referenced by:  sstr  2947  sstri  2948  sseq1  2960  sseq2  2961  ssun3  3102  ssun4  3103  ssinss1  3159  ssdisj  3271  triun  3858  trint0m  3862  sspwb  3943  exss  3954  relss  4370  funss  4863  funimass2  4920  fss  4997  bj-nntrans  9411
  Copyright terms: Public domain W3C validator