Theorem eqss 2957

Description: The subclass relationship is antisymmetric. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
eqss	⊢ (A = B ↔ (A ⊆ B ∧ B ⊆ A))

Proof of Theorem eqss

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		albiim 1376	. 2 ⊢ (∀x(x ∈ A ↔ x ∈ B) ↔ (∀x(x ∈ A → x ∈ B) ∧ ∀x(x ∈ B → x ∈ A)))
2		dfcleq 2034	. 2 ⊢ (A = B ↔ ∀x(x ∈ A ↔ x ∈ B))
3		dfss2 2931	. . 3 ⊢ (A ⊆ B ↔ ∀x(x ∈ A → x ∈ B))
4		dfss2 2931	. . 3 ⊢ (B ⊆ A ↔ ∀x(x ∈ B → x ∈ A))
5	3, 4	anbi12i 433	. 2 ⊢ ((A ⊆ B ∧ B ⊆ A) ↔ (∀x(x ∈ A → x ∈ B) ∧ ∀x(x ∈ B → x ∈ A)))
6	1, 2, 5	3bitr4i 201	1 ⊢ (A = B ↔ (A ⊆ B ∧ B ⊆ A))

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98  ∀wal 1241   = wceq 1243   ∈ wcel 1393   ⊆ wss 2914

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-11 1397  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-in 2921  df-ss 2928

This theorem is referenced by:  eqssi  2958  eqssd  2959  sseq1  2963  sseq2  2964  eqimss  2994  ssrabeq  3023  dfpss3  3027  uneqin  3185  ss0b  3253  vss  3261  sssnm  3519  unidif  3606  ssunieq  3607  iuneq1  3664  iuneq2  3667  iunxdif2  3699  ssext  3951  pweqb  3953  eqopab2b  4010  pwunim  4017  soeq2  4047  iunpw  4180  ordunisuc2r  4208  tfi  4251  eqrel  4375  eqrelrel  4387  coeq1  4439  coeq2  4440  cnveq  4455  dmeq  4481  relssres  4594  xp11m  4705  xpcanm  4706  xpcan2m  4707  ssrnres  4709  fnres  4961  eqfnfv3  5213  fneqeql2  5222  fconst4m  5327  f1imaeq  5360  eqoprab2b  5508  fo1stresm  5733  fo2ndresm  5734  nnacan  6025  nnmcan  6032  bj-sseq  9374  bdeq0  9430  bdvsn  9437  bdop  9438  bdeqsuc  9444  bj-om  9504