Theorem eqss 3212

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105  ∀wal 1371   = wceq 1373   ∈ wcel 2177   ⊆ wss 3170

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-in 3176  df-ss 3183

This theorem is referenced by:  eqssi  3213  eqssd  3214  sseq1  3220  sseq2  3221  eqimss  3251  ssrabeq  3284  uneqin  3428  ss0b  3504  vss  3512  sssnm  3800  unidif  3887  ssunieq  3888  iuneq1  3945  iuneq2  3948  iunxdif2  3981  ssext  4272  pweqb  4274  eqopab2b  4333  pwunim  4340  soeq2  4370  iunpw  4534  ordunisuc2r  4569  tfi  4637  eqrel  4771  eqrelrel  4783  coeq1  4842  coeq2  4843  cnveq  4859  dmeq  4886  relssres  5005  xp11m  5129  xpcanm  5130  xpcan2m  5131  ssrnres  5133  fnres  5401  eqfnfv3  5691  fneqeql2  5701  fconst4m  5816  f1imaeq  5856  eqoprab2b  6015  fo1stresm  6259  fo2ndresm  6260  nnacan  6610  nnmcan  6617  ixpeq2  6811  sbthlemi3  7075  wrdeq  11033  isprm2  12509  lssle0  14204  bastop1  14625  epttop  14632  opnneiid  14706  cnntr  14767  metequiv  15037  bj-sseq  15862  bdeq0  15937  bdvsn  15944  bdop  15945  bdeqsuc  15951  bj-om  16007