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

Theorem eqss 3813
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 1978 . 2 (∀𝑥(𝑥𝐴𝑥𝐵) ↔ (∀𝑥(𝑥𝐴𝑥𝐵) ∧ ∀𝑥(𝑥𝐵𝑥𝐴)))
2 dfcleq 2800 . 2 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
3 dfss2 3786 . . 3 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
4 dfss2 3786 . . 3 (𝐵𝐴 ↔ ∀𝑥(𝑥𝐵𝑥𝐴))
53, 4anbi12i 614 . 2 ((𝐴𝐵𝐵𝐴) ↔ (∀𝑥(𝑥𝐴𝑥𝐵) ∧ ∀𝑥(𝑥𝐵𝑥𝐴)))
61, 2, 53bitr4i 294 1 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  wal 1635   = wceq 1637  wcel 2156  wss 3769
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-in 3776  df-ss 3783
This theorem is referenced by:  eqssi  3814  eqssd  3815  sssseq  3816  sseq1  3823  sseq2  3824  eqimss  3854  ssrabeq  3887  dfpss3  3891  compleq  3951  uneqin  4080  pssdifn0  4145  ss0b  4171  vss  4210  pwpw0  4534  sssn  4547  ssunsn  4549  pwsnALT  4623  unidif  4665  ssunieq  4666  uniintsn  4706  iuneq1  4726  iuneq2  4729  iunxdif2  4760  ssext  5113  pweqb  5115  eqopab2b  5200  pwun  5217  soeq2  5252  eqrel  5411  eqrelrel  5423  coeq1  5481  coeq2  5482  cnveq  5497  dmeq  5525  relssres  5641  xp11  5780  ssrnres  5783  ordtri4  5973  oneqmini  5988  fnres  6214  eqfnfv3  6531  fneqeql2  6544  dff3  6590  fconst4  6699  f1imaeq  6742  eqoprab2b  6939  iunpw  7204  orduniorsuc  7256  tfi  7279  fo1stres  7420  fo2ndres  7421  wfrlem8  7654  tz7.49  7772  oawordeulem  7867  nnacan  7941  nnmcan  7947  ixpeq2  8155  sbthlem3  8307  isinf  8408  ordunifi  8445  inficl  8566  rankr1c  8927  rankc1  8976  iscard  9080  iscard2  9081  carden2  9092  aleph11  9186  cardaleph  9191  alephinit  9197  dfac12a  9251  cflm  9353  cfslb2n  9371  dfacfin7  9502  wrdeq  13534  isumltss  14798  rpnnen2lem12  15170  isprm2  15609  mrcidb2  16479  iscyggen2  18480  iscyg3  18485  lssle0  19150  islpir2  19456  iscss2  20236  ishil2  20269  bastop1  21007  epttop  21023  iscld4  21079  0ntr  21085  opnneiid  21140  isperf2  21166  cnntr  21289  ist1-3  21363  perfcls  21379  cmpfi  21421  isconn2  21427  dfconn2  21432  snfil  21877  filconn  21896  ufileu  21932  alexsubALTlem4  22063  metequiv  22523  nbuhgr2vtx1edgblem  26459  iscplgr  26534  shlesb1i  28569  shle0  28625  orthin  28629  chcon2i  28647  chcon3i  28649  chlejb1i  28659  chabs2  28700  h1datomi  28764  cmbr4i  28784  osumcor2i  28827  pjjsi  28883  pjin2i  29376  stcltr2i  29458  mdbr2  29479  dmdbr2  29486  mdsl2i  29505  mdsl2bi  29506  mdslmd3i  29515  chrelat4i  29556  sumdmdlem2  29602  dmdbr5ati  29605  eqrelrd2  29749  dfon2lem9  32011  idsset  32313  fneval  32663  topdifinfeq  33509  equivtotbnd  33883  heiborlem10  33925  eqrel2  34380  relcnveq3  34402  relcnveq2  34404  cossssid  34525  elrelscnveq3  34549  elrelscnveq2  34551  pmap11  35537  dia11N  36823  dia2dimlem5  36843  dib11N  36935  dih11  37040  dihglblem6  37115  doch11  37148  mapd11  37414  mapdcnv11N  37434  isnacs2  37765  mrefg3  37767  rababg  38373  relnonrel  38387  rcompleq  38812  uneqsn  38815  ntrk1k3eqk13  38842  ntrneineine1lem  38876  ntrneicls00  38881  ntrneixb  38887  ntrneik13  38890  ntrneix13  38891  prsal  41011
  Copyright terms: Public domain W3C validator