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

Theorem eqss 3610
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 1814 . 2 (∀𝑥(𝑥𝐴𝑥𝐵) ↔ (∀𝑥(𝑥𝐴𝑥𝐵) ∧ ∀𝑥(𝑥𝐵𝑥𝐴)))
2 dfcleq 2614 . 2 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
3 dfss2 3584 . . 3 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
4 dfss2 3584 . . 3 (𝐵𝐴 ↔ ∀𝑥(𝑥𝐵𝑥𝐴))
53, 4anbi12i 732 . 2 ((𝐴𝐵𝐵𝐴) ↔ (∀𝑥(𝑥𝐴𝑥𝐵) ∧ ∀𝑥(𝑥𝐵𝑥𝐴)))
61, 2, 53bitr4i 292 1 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  wal 1479   = wceq 1481  wcel 1988  wss 3567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-in 3574  df-ss 3581
This theorem is referenced by:  eqssi  3611  eqssd  3612  sssseq  3613  sseq1  3618  sseq2  3619  eqimss  3649  ssrabeq  3681  dfpss3  3685  compleq  3744  uneqin  3870  pssdifn0  3935  ss0b  3964  vss  4003  pwpw0  4335  sssn  4349  ssunsn  4351  pwsnALT  4420  unidif  4462  ssunieq  4463  uniintsn  4505  iuneq1  4525  iuneq2  4528  iunxdif2  4559  ssext  4914  pweqb  4916  eqopab2b  4995  pwun  5012  soeq2  5045  eqrel  5199  eqrelrel  5211  coeq1  5268  coeq2  5269  cnveq  5285  dmeq  5313  relssres  5425  xp11  5557  ssrnres  5560  ordtri4  5749  oneqmini  5764  fnres  5995  eqfnfv3  6299  fneqeql2  6312  dff3  6358  fconst4  6463  f1imaeq  6507  eqoprab2b  6698  iunpw  6963  orduniorsuc  7015  tfi  7038  fo1stres  7177  fo2ndres  7178  wfrlem8  7407  tz7.49  7525  oawordeulem  7619  nnacan  7693  nnmcan  7699  ixpeq2  7907  sbthlem3  8057  isinf  8158  ordunifi  8195  inficl  8316  rankr1c  8669  rankc1  8718  iscard  8786  iscard2  8787  carden2  8798  aleph11  8892  cardaleph  8897  alephinit  8903  dfac12a  8955  cflm  9057  cfslb2n  9075  dfacfin7  9206  wrdeq  13310  isumltss  14561  rpnnen2lem12  14935  isprm2  15376  mrcidb2  16259  iscyggen2  18264  iscyg3  18269  lssle0  18931  islpir2  19232  iscss2  20011  ishil2  20044  bastop1  20778  epttop  20794  iscld4  20850  0ntr  20856  opnneiid  20911  isperf2  20937  cnntr  21060  ist1-3  21134  perfcls  21150  cmpfi  21192  isconn2  21198  dfconn2  21203  snfil  21649  filconn  21668  ufileu  21704  alexsubALTlem4  21835  metequiv  22295  nbuhgr2vtx1edgblem  26228  shlesb1i  28215  shle0  28271  orthin  28275  chcon2i  28293  chcon3i  28295  chlejb1i  28305  chabs2  28346  h1datomi  28410  cmbr4i  28430  osumcor2i  28473  pjjsi  28529  pjin2i  29022  stcltr2i  29104  mdbr2  29125  dmdbr2  29132  mdsl2i  29151  mdsl2bi  29152  mdslmd3i  29161  chrelat4i  29202  sumdmdlem2  29248  dmdbr5ati  29251  eqrelrd2  29398  dfon2lem9  31670  idsset  31972  fneval  32322  topdifinfeq  33169  equivtotbnd  33548  heiborlem10  33590  pmap11  34867  dia11N  36156  dia2dimlem5  36176  dib11N  36268  dih11  36373  dihglblem6  36448  doch11  36481  mapd11  36747  mapdcnv11N  36767  isnacs2  37088  mrefg3  37090  rababg  37698  relnonrel  37712  rcompleq  38138  uneqsn  38141  ntrk1k3eqk13  38168  ntrneineine1lem  38202  ntrneicls00  38207  ntrneixb  38213  ntrneik13  38216  ntrneix13  38217  prsal  40301
  Copyright terms: Public domain W3C validator