Theorem eqss 3143

Description: The subclass relationship is antisymmetric. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
eqss	⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))

Proof of Theorem eqss

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		albiim 1467	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
2		dfcleq 2151	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		dfss2 3117	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		dfss2 3117	. . 3 ⊢ (𝐵 ⊆ 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴))
5	3, 4	anbi12i 456	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	1, 2, 5	3bitr4i 211	1 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104  ∀wal 1333   = wceq 1335   ∈ wcel 2128   ⊆ wss 3102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-11 1486  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-in 3108  df-ss 3115

This theorem is referenced by:  eqssi  3144  eqssd  3145  sseq1  3151  sseq2  3152  eqimss  3182  ssrabeq  3215  uneqin  3359  ss0b  3434  vss  3442  sssnm  3719  unidif  3806  ssunieq  3807  iuneq1  3864  iuneq2  3867  iunxdif2  3899  ssext  4183  pweqb  4185  eqopab2b  4241  pwunim  4248  soeq2  4278  iunpw  4442  ordunisuc2r  4475  tfi  4543  eqrel  4677  eqrelrel  4689  coeq1  4745  coeq2  4746  cnveq  4762  dmeq  4788  relssres  4906  xp11m  5026  xpcanm  5027  xpcan2m  5028  ssrnres  5030  fnres  5288  eqfnfv3  5569  fneqeql2  5578  fconst4m  5689  f1imaeq  5727  eqoprab2b  5881  fo1stresm  6111  fo2ndresm  6112  nnacan  6461  nnmcan  6468  ixpeq2  6659  sbthlemi3  6905  isprm2  12009  bastop1  12553  epttop  12560  opnneiid  12634  cnntr  12695  metequiv  12965  bj-sseq  13437  bdeq0  13513  bdvsn  13520  bdop  13521  bdeqsuc  13527  bj-om  13583