MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqss Structured version   Visualization version   GIF version

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

Proof of Theorem eqss
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 albiim 1965 . 2 (∀𝑥(𝑥𝐴𝑥𝐵) ↔ (∀𝑥(𝑥𝐴𝑥𝐵) ∧ ∀𝑥(𝑥𝐵𝑥𝐴)))
2 dfcleq 2754 . 2 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
3 dfss2 3732 . . 3 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
4 dfss2 3732 . . 3 (𝐵𝐴 ↔ ∀𝑥(𝑥𝐵𝑥𝐴))
53, 4anbi12i 735 . 2 ((𝐴𝐵𝐵𝐴) ↔ (∀𝑥(𝑥𝐴𝑥𝐵) ∧ ∀𝑥(𝑥𝐵𝑥𝐴)))
61, 2, 53bitr4i 292 1 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  wal 1630   = wceq 1632  wcel 2139  wss 3715
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-in 3722  df-ss 3729
This theorem is referenced by:  eqssi  3760  eqssd  3761  sssseq  3762  sseq1  3767  sseq2  3768  eqimss  3798  ssrabeq  3831  dfpss3  3835  compleq  3895  uneqin  4021  pssdifn0  4087  ss0b  4116  vss  4155  pwpw0  4489  sssn  4503  ssunsn  4505  pwsnALT  4581  unidif  4623  ssunieq  4624  uniintsn  4666  iuneq1  4686  iuneq2  4689  iunxdif2  4720  ssext  5072  pweqb  5074  eqopab2b  5155  pwun  5172  soeq2  5207  eqrel  5366  eqrelrel  5378  coeq1  5435  coeq2  5436  cnveq  5451  dmeq  5479  relssres  5595  xp11  5727  ssrnres  5730  ordtri4  5922  oneqmini  5937  fnres  6168  eqfnfv3  6476  fneqeql2  6489  dff3  6535  fconst4  6642  f1imaeq  6685  eqoprab2b  6878  iunpw  7143  orduniorsuc  7195  tfi  7218  fo1stres  7359  fo2ndres  7360  wfrlem8  7591  tz7.49  7709  oawordeulem  7803  nnacan  7877  nnmcan  7883  ixpeq2  8088  sbthlem3  8237  isinf  8338  ordunifi  8375  inficl  8496  rankr1c  8857  rankc1  8906  iscard  8991  iscard2  8992  carden2  9003  aleph11  9097  cardaleph  9102  alephinit  9108  dfac12a  9162  cflm  9264  cfslb2n  9282  dfacfin7  9413  wrdeq  13513  isumltss  14779  rpnnen2lem12  15153  isprm2  15597  mrcidb2  16480  iscyggen2  18483  iscyg3  18488  lssle0  19152  islpir2  19453  iscss2  20232  ishil2  20265  bastop1  20999  epttop  21015  iscld4  21071  0ntr  21077  opnneiid  21132  isperf2  21158  cnntr  21281  ist1-3  21355  perfcls  21371  cmpfi  21413  isconn2  21419  dfconn2  21424  snfil  21869  filconn  21888  ufileu  21924  alexsubALTlem4  22055  metequiv  22515  nbuhgr2vtx1edgblem  26446  iscplgr  26520  shlesb1i  28554  shle0  28610  orthin  28614  chcon2i  28632  chcon3i  28634  chlejb1i  28644  chabs2  28685  h1datomi  28749  cmbr4i  28769  osumcor2i  28812  pjjsi  28868  pjin2i  29361  stcltr2i  29443  mdbr2  29464  dmdbr2  29471  mdsl2i  29490  mdsl2bi  29491  mdslmd3i  29500  chrelat4i  29541  sumdmdlem2  29587  dmdbr5ati  29590  eqrelrd2  29735  dfon2lem9  32001  idsset  32303  fneval  32653  topdifinfeq  33509  equivtotbnd  33890  heiborlem10  33932  eqrel2  34392  relcnveq3  34416  relcnveq2  34418  cossssid  34540  elrelscnveq3  34564  elrelscnveq2  34566  pmap11  35551  dia11N  36839  dia2dimlem5  36859  dib11N  36951  dih11  37056  dihglblem6  37131  doch11  37164  mapd11  37430  mapdcnv11N  37450  isnacs2  37771  mrefg3  37773  rababg  38381  relnonrel  38395  rcompleq  38820  uneqsn  38823  ntrk1k3eqk13  38850  ntrneineine1lem  38884  ntrneicls00  38889  ntrneixb  38895  ntrneik13  38898  ntrneix13  38899  prsal  41041
  Copyright terms: Public domain W3C validator