Theorem eqss 3582

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.

Step	Hyp	Ref	Expression
1		albiim 1805	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
2		dfcleq 2603	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		dfss2 3556	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		dfss2 3556	. . 3 ⊢ (𝐵 ⊆ 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴))
5	3, 4	anbi12i 728	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	1, 2, 5	3bitr4i 290	1 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))

Syntax hints:   → wi 4   ↔ wb 194   ∧ wa 382  ∀wal 1472   = wceq 1474   ∈ wcel 1976   ⊆ wss 3539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-in 3546  df-ss 3553

This theorem is referenced by:  eqssi  3583  eqssd  3584  sseq1  3588  sseq2  3589  eqimss  3619  ssrabeq  3650  dfpss3  3654  compleq  3713  uneqin  3836  pssdifn0  3897  ss0b  3924  vss  3963  pwpw0  4283  sssn  4295  ssunsn  4297  pwsnALT  4361  unidif  4401  ssunieq  4402  uniintsn  4443  iuneq1  4464  iuneq2  4467  iunxdif2  4498  ssext  4843  pweqb  4845  eqopab2b  4919  pwun  4935  soeq2  4968  eqrel  5120  eqrelrel  5132  coeq1  5188  coeq2  5189  cnveq  5205  dmeq  5232  relssres  5343  xp11  5473  ssrnres  5476  ordtri4  5663  oneqmini  5678  fnres  5906  eqfnfv3  6205  fneqeql2  6218  dff3  6264  fconst4  6360  f1imaeq  6400  eqoprab2b  6588  iunpw  6847  orduniorsuc  6899  tfi  6922  fo1stres  7060  fo2ndres  7061  wfrlem8  7286  tz7.49  7404  oawordeulem  7498  nnacan  7572  nnmcan  7578  ixpeq2  7785  sbthlem3  7934  isinf  8035  ordunifi  8072  inficl  8191  rankr1c  8544  rankc1  8593  iscard  8661  iscard2  8662  carden2  8673  aleph11  8767  cardaleph  8772  alephinit  8778  dfac12a  8830  cflm  8932  cfslb2n  8950  dfacfin7  9081  wrdeq  13130  isumltss  14367  rpnnen2lem12  14741  isprm2  15181  mrcidb2  16049  iscyggen2  18054  iscyg3  18059  lssle0  18719  islpir2  19020  iscss2  19796  ishil2  19829  bastop1  20555  epttop  20570  iscld4  20626  0ntr  20632  opnneiid  20687  isperf2  20713  cnntr  20836  ist1-3  20910  perfcls  20926  cmpfi  20968  iscon2  20974  dfcon2  20979  snfil  21425  filcon  21444  ufileu  21480  alexsubALTlem4  21611  metequiv  22071  shlesb1i  27422  shle0  27478  orthin  27482  chcon2i  27500  chcon3i  27502  chlejb1i  27512  chabs2  27553  h1datomi  27617  cmbr4i  27637  osumcor2i  27680  pjjsi  27736  pjin2i  28229  stcltr2i  28311  mdbr2  28332  dmdbr2  28339  mdsl2i  28358  mdsl2bi  28359  mdslmd3i  28368  chrelat4i  28409  sumdmdlem2  28455  dmdbr5ati  28458  eqrelrd2  28599  dfon2lem9  30733  idsset  30960  fneval  31310  topdifinfeq  32157  equivtotbnd  32530  heiborlem10  32572  pmap11  33849  dia11N  35138  dia2dimlem5  35158  dib11N  35250  dih11  35355  dihglblem6  35430  doch11  35463  mapd11  35729  mapdcnv11N  35749  isnacs2  36070  mrefg3  36072  rababg  36681  relnonrel  36695  rcompleq  37121  uneqsn  37124  ntrk1k3eqk13  37151  ntrneineine1lem  37185  ntrneicls00  37190  ntrneixb  37196  ntrneik13  37199  ntrneix13  37200  prsal  38997  sssseq  40089  nbuhgr2vtx1edgblem  40554