Theorem eqss 3182

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 1497	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
2		dfcleq 2181	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		dfss2 3156	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		dfss2 3156	. . 3 ⊢ (𝐵 ⊆ 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴))
5	3, 4	anbi12i 460	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	1, 2, 5	3bitr4i 212	1 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105  ∀wal 1361   = wceq 1363   ∈ wcel 2158   ⊆ wss 3141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-11 1516  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-in 3147  df-ss 3154

This theorem is referenced by:  eqssi  3183  eqssd  3184  sseq1  3190  sseq2  3191  eqimss  3221  ssrabeq  3254  uneqin  3398  ss0b  3474  vss  3482  sssnm  3766  unidif  3853  ssunieq  3854  iuneq1  3911  iuneq2  3914  iunxdif2  3947  ssext  4233  pweqb  4235  eqopab2b  4291  pwunim  4298  soeq2  4328  iunpw  4492  ordunisuc2r  4525  tfi  4593  eqrel  4727  eqrelrel  4739  coeq1  4796  coeq2  4797  cnveq  4813  dmeq  4839  relssres  4957  xp11m  5079  xpcanm  5080  xpcan2m  5081  ssrnres  5083  fnres  5344  eqfnfv3  5628  fneqeql2  5638  fconst4m  5749  f1imaeq  5789  eqoprab2b  5946  fo1stresm  6176  fo2ndresm  6177  nnacan  6527  nnmcan  6534  ixpeq2  6726  sbthlemi3  6972  isprm2  12131  lssle0  13561  bastop1  13879  epttop  13886  opnneiid  13960  cnntr  14021  metequiv  14291  bj-sseq  14840  bdeq0  14915  bdvsn  14922  bdop  14923  bdeqsuc  14929  bj-om  14985