Theorem eqss 3117

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

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104  ∀wal 1330   = wceq 1332   ∈ wcel 1481   ⊆ wss 3076

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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-11 1485  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-in 3082  df-ss 3089

This theorem is referenced by:  eqssi  3118  eqssd  3119  sseq1  3125  sseq2  3126  eqimss  3156  ssrabeq  3188  uneqin  3332  ss0b  3407  vss  3415  sssnm  3689  unidif  3776  ssunieq  3777  iuneq1  3834  iuneq2  3837  iunxdif2  3869  ssext  4151  pweqb  4153  eqopab2b  4209  pwunim  4216  soeq2  4246  iunpw  4409  ordunisuc2r  4438  tfi  4504  eqrel  4636  eqrelrel  4648  coeq1  4704  coeq2  4705  cnveq  4721  dmeq  4747  relssres  4865  xp11m  4985  xpcanm  4986  xpcan2m  4987  ssrnres  4989  fnres  5247  eqfnfv3  5528  fneqeql2  5537  fconst4m  5648  f1imaeq  5684  eqoprab2b  5837  fo1stresm  6067  fo2ndresm  6068  nnacan  6416  nnmcan  6423  ixpeq2  6614  sbthlemi3  6855  isprm2  11834  bastop1  12291  epttop  12298  opnneiid  12372  cnntr  12433  metequiv  12703  bj-sseq  13170  bdeq0  13236  bdvsn  13243  bdop  13244  bdeqsuc  13250  bj-om  13306