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

Theorem eqss 3162
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 1480 . 2 (∀𝑥(𝑥𝐴𝑥𝐵) ↔ (∀𝑥(𝑥𝐴𝑥𝐵) ∧ ∀𝑥(𝑥𝐵𝑥𝐴)))
2 dfcleq 2164 . 2 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
3 dfss2 3136 . . 3 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
4 dfss2 3136 . . 3 (𝐵𝐴 ↔ ∀𝑥(𝑥𝐵𝑥𝐴))
53, 4anbi12i 457 . 2 ((𝐴𝐵𝐵𝐴) ↔ (∀𝑥(𝑥𝐴𝑥𝐵) ∧ ∀𝑥(𝑥𝐵𝑥𝐴)))
61, 2, 53bitr4i 211 1 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  wal 1346   = wceq 1348  wcel 2141  wss 3121
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 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152
This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134
This theorem is referenced by:  eqssi  3163  eqssd  3164  sseq1  3170  sseq2  3171  eqimss  3201  ssrabeq  3234  uneqin  3378  ss0b  3454  vss  3462  sssnm  3741  unidif  3828  ssunieq  3829  iuneq1  3886  iuneq2  3889  iunxdif2  3921  ssext  4206  pweqb  4208  eqopab2b  4264  pwunim  4271  soeq2  4301  iunpw  4465  ordunisuc2r  4498  tfi  4566  eqrel  4700  eqrelrel  4712  coeq1  4768  coeq2  4769  cnveq  4785  dmeq  4811  relssres  4929  xp11m  5049  xpcanm  5050  xpcan2m  5051  ssrnres  5053  fnres  5314  eqfnfv3  5595  fneqeql2  5605  fconst4m  5716  f1imaeq  5754  eqoprab2b  5911  fo1stresm  6140  fo2ndresm  6141  nnacan  6491  nnmcan  6498  ixpeq2  6690  sbthlemi3  6936  isprm2  12071  bastop1  12877  epttop  12884  opnneiid  12958  cnntr  13019  metequiv  13289  bj-sseq  13827  bdeq0  13902  bdvsn  13909  bdop  13910  bdeqsuc  13916  bj-om  13972
  Copyright terms: Public domain W3C validator