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

Theorem eqss 2954
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 1373 . 2 (x(x Ax B) ↔ (x(x Ax B) x(x Bx A)))
2 dfcleq 2031 . 2 (A = Bx(x Ax B))
3 dfss2 2928 . . 3 (ABx(x Ax B))
4 dfss2 2928 . . 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 1240   = wceq 1242   wcel 1390  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:  eqssi  2955  eqssd  2956  sseq1  2960  sseq2  2961  eqimss  2991  ssrabeq  3020  dfpss3  3024  uneqin  3182  ss0b  3250  vss  3258  sssnm  3516  unidif  3603  ssunieq  3604  iuneq1  3661  iuneq2  3664  iunxdif2  3696  ssext  3948  pweqb  3950  eqopab2b  4007  pwunim  4014  soeq2  4044  iunpw  4177  ordunisuc2r  4205  tfi  4248  eqrel  4372  eqrelrel  4384  coeq1  4436  coeq2  4437  cnveq  4452  dmeq  4478  relssres  4591  xp11m  4702  xpcanm  4703  xpcan2m  4704  ssrnres  4706  fnres  4958  eqfnfv3  5210  fneqeql2  5219  fconst4m  5324  f1imaeq  5357  eqoprab2b  5505  fo1stresm  5730  fo2ndresm  5731  nnacan  6021  nnmcan  6028  bj-sseq  9266  bdeq0  9322  bdvsn  9329  bdop  9330  bdeqsuc  9336  bj-om  9396
  Copyright terms: Public domain W3C validator