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

Theorem eqss 3080
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 1446 . 2 (∀𝑥(𝑥𝐴𝑥𝐵) ↔ (∀𝑥(𝑥𝐴𝑥𝐵) ∧ ∀𝑥(𝑥𝐵𝑥𝐴)))
2 dfcleq 2109 . 2 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
3 dfss2 3054 . . 3 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
4 dfss2 3054 . . 3 (𝐵𝐴 ↔ ∀𝑥(𝑥𝐵𝑥𝐴))
53, 4anbi12i 453 . 2 ((𝐴𝐵𝐵𝐴) ↔ (∀𝑥(𝑥𝐴𝑥𝐵) ∧ ∀𝑥(𝑥𝐵𝑥𝐴)))
61, 2, 53bitr4i 211 1 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  wal 1312   = wceq 1314  wcel 1463  wss 3039
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 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-11 1467  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-in 3045  df-ss 3052
This theorem is referenced by:  eqssi  3081  eqssd  3082  sseq1  3088  sseq2  3089  eqimss  3119  ssrabeq  3151  uneqin  3295  ss0b  3370  vss  3378  sssnm  3649  unidif  3736  ssunieq  3737  iuneq1  3794  iuneq2  3797  iunxdif2  3829  ssext  4111  pweqb  4113  eqopab2b  4169  pwunim  4176  soeq2  4206  iunpw  4369  ordunisuc2r  4398  tfi  4464  eqrel  4596  eqrelrel  4608  coeq1  4664  coeq2  4665  cnveq  4681  dmeq  4707  relssres  4825  xp11m  4945  xpcanm  4946  xpcan2m  4947  ssrnres  4949  fnres  5207  eqfnfv3  5486  fneqeql2  5495  fconst4m  5606  f1imaeq  5642  eqoprab2b  5795  fo1stresm  6025  fo2ndresm  6026  nnacan  6374  nnmcan  6381  ixpeq2  6572  sbthlemi3  6813  isprm2  11705  bastop1  12158  epttop  12165  opnneiid  12239  cnntr  12300  metequiv  12570  bj-sseq  12833  bdeq0  12899  bdvsn  12906  bdop  12907  bdeqsuc  12913  bj-om  12969
  Copyright terms: Public domain W3C validator