Theorem eqss 3198

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105  ∀wal 1362   = wceq 1364   ∈ wcel 2167   ⊆ wss 3157

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  eqssi  3199  eqssd  3200  sseq1  3206  sseq2  3207  eqimss  3237  ssrabeq  3270  uneqin  3414  ss0b  3490  vss  3498  sssnm  3784  unidif  3871  ssunieq  3872  iuneq1  3929  iuneq2  3932  iunxdif2  3965  ssext  4254  pweqb  4256  eqopab2b  4314  pwunim  4321  soeq2  4351  iunpw  4515  ordunisuc2r  4550  tfi  4618  eqrel  4752  eqrelrel  4764  coeq1  4823  coeq2  4824  cnveq  4840  dmeq  4866  relssres  4984  xp11m  5108  xpcanm  5109  xpcan2m  5110  ssrnres  5112  fnres  5374  eqfnfv3  5661  fneqeql2  5671  fconst4m  5782  f1imaeq  5822  eqoprab2b  5980  fo1stresm  6219  fo2ndresm  6220  nnacan  6570  nnmcan  6577  ixpeq2  6771  sbthlemi3  7025  wrdeq  10957  isprm2  12285  lssle0  13928  bastop1  14319  epttop  14326  opnneiid  14400  cnntr  14461  metequiv  14731  bj-sseq  15438  bdeq0  15513  bdvsn  15520  bdop  15521  bdeqsuc  15527  bj-om  15583