Theorem eqss 3583

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 1806	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
2		dfcleq 2604	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		dfss2 3557	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		dfss2 3557	. . 3 ⊢ (𝐵 ⊆ 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴))
5	3, 4	anbi12i 729	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	1, 2, 5	3bitr4i 291	1 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383  ∀wal 1473   = wceq 1475   ∈ wcel 1977   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554

This theorem is referenced by:  eqssi  3584  eqssd  3585  sseq1  3589  sseq2  3590  eqimss  3620  ssrabeq  3651  dfpss3  3655  compleq  3714  uneqin  3837  pssdifn0  3898  ss0b  3925  vss  3964  pwpw0  4284  sssn  4298  ssunsn  4300  pwsnALT  4367  unidif  4407  ssunieq  4408  uniintsn  4449  iuneq1  4470  iuneq2  4473  iunxdif2  4504  ssext  4850  pweqb  4852  eqopab2b  4930  pwun  4946  soeq2  4979  eqrel  5132  eqrelrel  5144  coeq1  5201  coeq2  5202  cnveq  5218  dmeq  5246  relssres  5357  xp11  5488  ssrnres  5491  ordtri4  5678  oneqmini  5693  fnres  5921  eqfnfv3  6221  fneqeql2  6234  dff3  6280  fconst4  6383  f1imaeq  6423  eqoprab2b  6611  iunpw  6870  orduniorsuc  6922  tfi  6945  fo1stres  7083  fo2ndres  7084  wfrlem8  7309  tz7.49  7427  oawordeulem  7521  nnacan  7595  nnmcan  7601  ixpeq2  7808  sbthlem3  7957  isinf  8058  ordunifi  8095  inficl  8214  rankr1c  8567  rankc1  8616  iscard  8684  iscard2  8685  carden2  8696  aleph11  8790  cardaleph  8795  alephinit  8801  dfac12a  8853  cflm  8955  cfslb2n  8973  dfacfin7  9104  wrdeq  13182  isumltss  14419  rpnnen2lem12  14793  isprm2  15233  mrcidb2  16101  iscyggen2  18106  iscyg3  18111  lssle0  18771  islpir2  19072  iscss2  19849  ishil2  19882  bastop1  20608  epttop  20623  iscld4  20679  0ntr  20685  opnneiid  20740  isperf2  20766  cnntr  20889  ist1-3  20963  perfcls  20979  cmpfi  21021  iscon2  21027  dfcon2  21032  snfil  21478  filcon  21497  ufileu  21533  alexsubALTlem4  21664  metequiv  22124  shlesb1i  27629  shle0  27685  orthin  27689  chcon2i  27707  chcon3i  27709  chlejb1i  27719  chabs2  27760  h1datomi  27824  cmbr4i  27844  osumcor2i  27887  pjjsi  27943  pjin2i  28436  stcltr2i  28518  mdbr2  28539  dmdbr2  28546  mdsl2i  28565  mdsl2bi  28566  mdslmd3i  28575  chrelat4i  28616  sumdmdlem2  28662  dmdbr5ati  28665  eqrelrd2  28806  dfon2lem9  30940  idsset  31167  fneval  31517  topdifinfeq  32374  equivtotbnd  32747  heiborlem10  32789  pmap11  34066  dia11N  35355  dia2dimlem5  35375  dib11N  35467  dih11  35572  dihglblem6  35647  doch11  35680  mapd11  35946  mapdcnv11N  35966  isnacs2  36287  mrefg3  36289  rababg  36898  relnonrel  36912  rcompleq  37338  uneqsn  37341  ntrk1k3eqk13  37368  ntrneineine1lem  37402  ntrneicls00  37407  ntrneixb  37413  ntrneik13  37416  ntrneix13  37417  prsal  39214  sssseq  40305  nbuhgr2vtx1edgblem  40573