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

Theorem eqss 2957
Description: The subclass relationship is antisymmetric. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
eqss (A = B ↔ (AB BA))

Proof of Theorem eqss
Dummy variable x is distinct from all other variables.
StepHypRef Expression
1 albiim 1376 . 2 (x(x Ax B) ↔ (x(x Ax B) x(x Bx A)))
2 dfcleq 2034 . 2 (A = Bx(x Ax B))
3 dfss2 2931 . . 3 (ABx(x Ax B))
4 dfss2 2931 . . 3 (BAx(x Bx A))
53, 4anbi12i 433 . 2 ((AB BA) ↔ (x(x Ax B) x(x Bx A)))
61, 2, 53bitr4i 201 1 (A = B ↔ (AB BA))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98  wal 1241   = wceq 1243   wcel 1393  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:  eqssi  2958  eqssd  2959  sseq1  2963  sseq2  2964  eqimss  2994  ssrabeq  3023  dfpss3  3027  uneqin  3185  ss0b  3253  vss  3261  sssnm  3519  unidif  3606  ssunieq  3607  iuneq1  3664  iuneq2  3667  iunxdif2  3699  ssext  3951  pweqb  3953  eqopab2b  4010  pwunim  4017  soeq2  4047  iunpw  4180  ordunisuc2r  4208  tfi  4251  eqrel  4375  eqrelrel  4387  coeq1  4439  coeq2  4440  cnveq  4455  dmeq  4481  relssres  4594  xp11m  4705  xpcanm  4706  xpcan2m  4707  ssrnres  4709  fnres  4961  eqfnfv3  5213  fneqeql2  5222  fconst4m  5327  f1imaeq  5360  eqoprab2b  5508  fo1stresm  5733  fo2ndresm  5734  nnacan  6025  nnmcan  6032  bj-sseq  9374  bdeq0  9430  bdvsn  9437  bdop  9438  bdeqsuc  9444  bj-om  9504
  Copyright terms: Public domain W3C validator