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

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

Proof of Theorem eqss
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 albiim 1467 . 2 (∀𝑥(𝑥𝐴𝑥𝐵) ↔ (∀𝑥(𝑥𝐴𝑥𝐵) ∧ ∀𝑥(𝑥𝐵𝑥𝐴)))
2 dfcleq 2151 . 2 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
3 dfss2 3117 . . 3 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
4 dfss2 3117 . . 3 (𝐵𝐴 ↔ ∀𝑥(𝑥𝐵𝑥𝐴))
53, 4anbi12i 456 . 2 ((𝐴𝐵𝐵𝐴) ↔ (∀𝑥(𝑥𝐴𝑥𝐵) ∧ ∀𝑥(𝑥𝐵𝑥𝐴)))
61, 2, 53bitr4i 211 1 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  wal 1333   = wceq 1335  wcel 2128  wss 3102
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-11 1486  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139
This theorem depends on definitions:  df-bi 116  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-in 3108  df-ss 3115
This theorem is referenced by:  eqssi  3144  eqssd  3145  sseq1  3151  sseq2  3152  eqimss  3182  ssrabeq  3215  uneqin  3359  ss0b  3434  vss  3442  sssnm  3719  unidif  3806  ssunieq  3807  iuneq1  3864  iuneq2  3867  iunxdif2  3899  ssext  4183  pweqb  4185  eqopab2b  4241  pwunim  4248  soeq2  4278  iunpw  4442  ordunisuc2r  4475  tfi  4543  eqrel  4677  eqrelrel  4689  coeq1  4745  coeq2  4746  cnveq  4762  dmeq  4788  relssres  4906  xp11m  5026  xpcanm  5027  xpcan2m  5028  ssrnres  5030  fnres  5288  eqfnfv3  5569  fneqeql2  5578  fconst4m  5689  f1imaeq  5727  eqoprab2b  5881  fo1stresm  6111  fo2ndresm  6112  nnacan  6461  nnmcan  6468  ixpeq2  6659  sbthlemi3  6905  isprm2  12009  bastop1  12553  epttop  12560  opnneiid  12634  cnntr  12695  metequiv  12965  bj-sseq  13437  bdeq0  13513  bdvsn  13520  bdop  13521  bdeqsuc  13527  bj-om  13583
  Copyright terms: Public domain W3C validator