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

Theorem eqss 3930
 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 1890 . 2 (∀𝑥(𝑥𝐴𝑥𝐵) ↔ (∀𝑥(𝑥𝐴𝑥𝐵) ∧ ∀𝑥(𝑥𝐵𝑥𝐴)))
2 dfcleq 2792 . 2 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
3 dfss2 3901 . . 3 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
4 dfss2 3901 . . 3 (𝐵𝐴 ↔ ∀𝑥(𝑥𝐵𝑥𝐴))
53, 4anbi12i 629 . 2 ((𝐴𝐵𝐵𝐴) ↔ (∀𝑥(𝑥𝐴𝑥𝐵) ∧ ∀𝑥(𝑥𝐵𝑥𝐴)))
61, 2, 53bitr4i 306 1 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1536   = wceq 1538   ∈ wcel 2111   ⊆ wss 3881 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898 This theorem is referenced by:  eqssi  3931  eqssd  3932  sssseq  3933  sseq1  3940  sseq2  3941  eqimss  3971  ssrabeq  4010  dfpss3  4014  compleq  4075  uneqin  4205  rcompleq  4220  pssdifn0  4279  ss0b  4305  vss  4351  pwpw0  4706  sssn  4719  ssunsn  4721  pwsnOLD  4794  unidif  4835  ssunieq  4836  uniintsn  4876  iuneq1  4898  iuneq2  4901  iunxdif2  4941  ssext  5313  pweqb  5315  eqopab2bw  5401  eqopab2b  5405  pwun  5424  soeq2  5460  eqrel  5623  eqrelrel  5635  coeq1  5693  coeq2  5694  cnveq  5709  dmeq  5737  relssres  5860  xp11  6000  ssrnres  6003  ordtri4  6199  oneqmini  6213  fnres  6449  eqfnfv3  6786  fneqeql2  6799  dff3  6848  fconst4  6959  f1imaeq  7006  eqoprab2bw  7208  eqoprab2b  7209  iunpw  7480  orduniorsuc  7532  tfi  7555  fo1stres  7704  fo2ndres  7705  wfrlem8  7952  tz7.49  8071  oawordeulem  8170  nnacan  8244  nnmcan  8250  ixpeq2  8465  sbthlem3  8620  isinf  8722  ordunifi  8759  inficl  8880  rankr1c  9241  rankc1  9290  iscard  9395  iscard2  9396  carden2  9407  aleph11  9502  cardaleph  9507  alephinit  9513  dfac12a  9566  cflm  9668  cfslb2n  9686  dfacfin7  9817  wrdeq  13886  isumltss  15202  rpnnen2lem12  15577  isprm2  16023  mrcidb2  16888  smndex2dnrinv  18079  iscyggen2  19001  iscyg3  19006  lssle0  19722  islpir2  20025  iscss2  20384  ishil2  20417  bastop1  21612  epttop  21628  iscld4  21684  0ntr  21690  opnneiid  21745  isperf2  21771  cnntr  21894  ist1-3  21968  perfcls  21984  cmpfi  22027  isconn2  22033  dfconn2  22038  snfil  22483  filconn  22502  ufileu  22538  alexsubALTlem4  22669  metequiv  23130  nbuhgr2vtx1edgblem  27155  iscplgr  27219  shlesb1i  29183  shle0  29239  orthin  29243  chcon2i  29261  chcon3i  29263  chlejb1i  29273  chabs2  29314  h1datomi  29378  cmbr4i  29398  osumcor2i  29441  pjjsi  29497  pjin2i  29990  stcltr2i  30072  mdbr2  30093  dmdbr2  30100  mdsl2i  30119  mdsl2bi  30120  mdslmd3i  30129  chrelat4i  30170  sumdmdlem2  30216  dmdbr5ati  30219  eqdif  30304  eqrelrd2  30394  dfon2lem9  33185  idsset  33500  fneval  33849  topdifinfeq  34807  equivtotbnd  35256  heiborlem10  35298  eqrel2  35757  relcnveq3  35778  relcnveq2  35780  cossssid  35907  elrelscnveq3  35931  elrelscnveq2  35933  pmap11  37098  dia11N  38384  dia2dimlem5  38404  dib11N  38496  dih11  38601  dihglblem6  38676  doch11  38709  mapd11  38975  mapdcnv11N  38995  isnacs2  39711  mrefg3  39713  ontric3g  40294  rababg  40337  relnonrel  40351  uneqsn  40790  ntrk1k3eqk13  40817  ntrneineine1lem  40851  ntrneicls00  40856  ntrneixb  40862  ntrneik13  40865  ntrneix13  40866
 Copyright terms: Public domain W3C validator