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

Theorem eqss 2937
Description: The subclass relationship is antisymmetric. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
eqss 
C_  C_

Proof of Theorem eqss
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 albiim 1357 . 2
2 dfcleq 2016 . 2
3 dfss2 2911 . . 3 
C_
4 dfss2 2911 . . 3 
C_
53, 4anbi12i 436 . 2  C_  C_
61, 2, 53bitr4i 201 1 
C_  C_
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97   wb 98  wal 1226   wceq 1228   wcel 1374    C_ wss 2894
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 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-11 1378  ax-4 1381  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-nf 1330  df-sb 1628  df-clab 2009  df-cleq 2015  df-clel 2018  df-in 2901  df-ss 2908
This theorem is referenced by:  eqssi  2938  eqssd  2939  sseq1  2943  sseq2  2944  eqimss  2974  ssrabeq  3003  dfpss3  3007  uneqin  3165  ss0b  3233  vss  3241  sssnm  3499  unidif  3586  ssunieq  3587  iuneq1  3644  iuneq2  3647  iunxdif2  3679  ssext  3931  pweqb  3933  eqopab2b  3990  pwunim  3997  soeq2  4027  iunpw  4161  ordunisuc2r  4189  tfi  4232  eqrel  4356  eqrelrel  4368  coeq1  4420  coeq2  4421  cnveq  4436  dmeq  4462  relssres  4575  xp11m  4686  xpcanm  4687  xpcan2m  4688  ssrnres  4690  fnres  4941  eqfnfv3  5192  fneqeql2  5201  fconst4m  5306  f1imaeq  5339  eqoprab2b  5486  fo1stresm  5711  fo2ndresm  5712  nnacan  5996  nnmcan  6003  bj-sseq  7038  bdeq0  7094  bdvsn  7101  bdop  7102  bdeqsuc  7108  bj-om  7159
  Copyright terms: Public domain W3C validator