Theorem eqss 3242

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105  ∀wal 1395   = wceq 1397   ∈ wcel 2202   ⊆ wss 3200

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  eqssi  3243  eqssd  3244  sseq1  3250  sseq2  3251  eqimss  3281  ssrabeq  3314  uneqin  3458  ss0b  3534  vss  3542  sssnm  3837  unidif  3925  ssunieq  3926  iuneq1  3983  iuneq2  3986  iunxdif2  4019  ssext  4313  pweqb  4315  eqopab2b  4374  pwunim  4383  soeq2  4413  iunpw  4577  ordunisuc2r  4612  tfi  4680  eqrel  4815  eqrelrel  4827  coeq1  4887  coeq2  4888  cnveq  4904  dmeq  4931  relssres  5051  xp11m  5175  xpcanm  5176  xpcan2m  5177  ssrnres  5179  fnres  5449  eqfnfv3  5746  fneqeql2  5756  fconst4m  5874  f1imaeq  5916  eqoprab2b  6079  fo1stresm  6324  fo2ndresm  6325  nnacan  6680  nnmcan  6687  ixpeq2  6881  sbthlemi3  7158  wrdeq  11139  isprm2  12694  lssle0  14392  bastop1  14813  epttop  14820  opnneiid  14894  cnntr  14955  metequiv  15225  bj-sseq  16414  bdeq0  16488  bdvsn  16495  bdop  16496  bdeqsuc  16502  bj-om  16558