Theorem eqss 3263

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105  ∀wal 1400   = wceq 1402   ∈ wcel 2209   ⊆ wss 3220

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is referenced by:  eqssi  3264  eqssd  3265  sseq1  3271  sseq2  3272  eqimss  3302  ssrabeq  3336  uneqin  3482  ss0b  3562  vss  3568  sssnm  3877  unidif  3965  ssunieq  3966  iuneq1  4023  iuneq2  4026  iunxdif2  4059  ssext  4359  pweqb  4361  eqopab2b  4420  pwunim  4429  soeq2  4459  iunpw  4624  ordunisuc2r  4659  tfi  4727  eqrel  4862  eqrelrel  4874  coeq1  4935  coeq2  4936  cnveq  4952  dmeq  4979  relssres  5099  xp11m  5224  xpcanm  5225  xpcan2m  5226  ssrnres  5228  fnres  5498  eqfnfv3  5802  fneqeql2  5812  fconst4m  5929  f1imaeq  5975  eqoprab2b  6140  fo1stresm  6389  fo2ndresm  6390  nnacan  6779  nnmcan  6786  ixpeq2  6988  sbthlemi3  7270  wrdeq  11309  isprm2  12878  lssle0  14692  bastop1  15167  epttop  15174  opnneiid  15248  cnntr  15309  metequiv  15579  bj-sseq  16803  bdeq0  16876  bdvsn  16883  bdop  16884  bdeqsuc  16890  bj-om  16946