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

Theorem dfss3 2932
Description: Alternate definition of subclass relationship. (Contributed by NM, 14-Oct-1999.)
Assertion
Ref Expression
dfss3 
C_
Distinct variable groups:   ,   ,

Proof of Theorem dfss3
StepHypRef Expression
1 dfss2 2931 . 2 
C_
2 df-ral 2308 . 2
31, 2bitr4i 176 1 
C_
Colors of variables: wff set class
Syntax hints:   wi 4   wb 98  wal 1241   wcel 1393  wral 2303    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-ral 2308  df-in 2921  df-ss 2928
This theorem is referenced by:  ssrab  3015  eqsnm  3520  uni0b  3599  uni0c  3600  ssint  3625  ssiinf  3700  sspwuni  3733  dftr3  3852  tfis  4252  rninxp  4710  fnres  4961  eqfnfv3  5213  funimass3  5229  ffvresb  5274  tfrlemibxssdm  5886  bdss  9427
  Copyright terms: Public domain W3C validator