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

Theorem eqss 2935
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 1357 . 2 (x(x Ax B) ↔ (x(x Ax B) x(x Bx A)))
2 dfcleq 2016 . 2 (A = Bx(x Ax B))
3 dfss2 2909 . . 3 (ABx(x Ax B))
4 dfss2 2909 . . 3 (BAx(x Bx A))
53, 4anbi12i 436 . 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 1226   = wceq 1228   wcel 1374  wss 2892
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 2899  df-ss 2906
This theorem is referenced by:  eqssi  2936  eqssd  2937  sseq1  2941  sseq2  2942  eqimss  2972  ssrabeq  3001  dfpss3  3005  uneqin  3163  ss0b  3231  vss  3239  sssnm  3497  unidif  3584  ssunieq  3585  iuneq1  3642  iuneq2  3645  iunxdif2  3677  ssext  3929  pweqb  3931  eqopab2b  3988  pwunim  3995  soeq2  4025  iunpw  4159  ordunisuc2r  4187  tfi  4230  eqrel  4354  eqrelrel  4366  coeq1  4418  coeq2  4419  cnveq  4434  dmeq  4460  relssres  4573  xp11m  4684  xpcanm  4685  xpcan2m  4686  ssrnres  4688  fnres  4939  eqfnfv3  5190  fneqeql2  5199  fconst4m  5304  f1imaeq  5337  eqoprab2b  5484  fo1stresm  5709  fo2ndresm  5710  nnacan  5994  nnmcan  6001  bj-sseq  6717  bdeq0  6773  bdvsn  6780  bdop  6781  bdeqsuc  6787  bj-om  6838
  Copyright terms: Public domain W3C validator