Theorem eqss 3162

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 1480	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
2		dfcleq 2164	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		dfss2 3136	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		dfss2 3136	. . 3 ⊢ (𝐵 ⊆ 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴))
5	3, 4	anbi12i 457	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	1, 2, 5	3bitr4i 211	1 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104  ∀wal 1346   = wceq 1348   ∈ wcel 2141   ⊆ wss 3121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134

This theorem is referenced by:  eqssi  3163  eqssd  3164  sseq1  3170  sseq2  3171  eqimss  3201  ssrabeq  3234  uneqin  3378  ss0b  3454  vss  3462  sssnm  3741  unidif  3828  ssunieq  3829  iuneq1  3886  iuneq2  3889  iunxdif2  3921  ssext  4206  pweqb  4208  eqopab2b  4264  pwunim  4271  soeq2  4301  iunpw  4465  ordunisuc2r  4498  tfi  4566  eqrel  4700  eqrelrel  4712  coeq1  4768  coeq2  4769  cnveq  4785  dmeq  4811  relssres  4929  xp11m  5049  xpcanm  5050  xpcan2m  5051  ssrnres  5053  fnres  5314  eqfnfv3  5595  fneqeql2  5605  fconst4m  5716  f1imaeq  5754  eqoprab2b  5911  fo1stresm  6140  fo2ndresm  6141  nnacan  6491  nnmcan  6498  ixpeq2  6690  sbthlemi3  6936  isprm2  12071  bastop1  12877  epttop  12884  opnneiid  12958  cnntr  13019  metequiv  13289  bj-sseq  13827  bdeq0  13902  bdvsn  13909  bdop  13910  bdeqsuc  13916  bj-om  13972