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

Theorem dfss2 2931
Description: Alternate definition of the subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. (Contributed by NM, 8-Jan-2002.)
Assertion
Ref Expression
dfss2 
C_
Distinct variable groups:   ,   ,

Proof of Theorem dfss2
StepHypRef Expression
1 dfss 2929 . . 3 
C_  i^i
2 df-in 2921 . . . 4  i^i  {  |  }
32eqeq2i 2050 . . 3  i^i  {  |  }
4 abeq2 2146 . . 3  {  |  }
51, 3, 43bitri 195 . 2 
C_
6 pm4.71 369 . . 3
76albii 1359 . 2
85, 7bitr4i 176 1 
C_
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97   wb 98  wal 1241   wceq 1243   wcel 1393   {cab 2026    i^i cin 2913    C_ wss 2914
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 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-11 1397  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-in 2921  df-ss 2928
This theorem is referenced by:  dfss3  2932  dfss2f  2933  ssel  2936  ssriv  2946  ssrdv  2948  sstr2  2949  eqss  2957  nssr  3000  rabss2  3020  ssconb  3073  ssequn1  3110  unss  3114  ssin  3156  ssddif  3168  reldisj  3268  ssdif0im  3283  inssdif0im  3288  ssundifim  3303  sbcssg  3327  pwss  3369  snss  3488  snsssn  3526  ssuni  3596  unissb  3604  intss  3630  iunss  3692  dftr2  3850  axpweq  3918  axpow2  3923  ssextss  3950  ordunisuc2r  4208  setind  4225  tfi  4251  ssrel  4374  ssrel2  4376  ssrelrel  4386  reliun  4404  relop  4432  issref  4653  funimass4  5170  bj-inf2vnlem3  9540  bj-inf2vnlem4  9541
  Copyright terms: Public domain W3C validator