Theorem eqss 2931

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 1352	. 2 ⊢ (∀x(x ∈ A ↔ x ∈ B) ↔ (∀x(x ∈ A → x ∈ B) ∧ ∀x(x ∈ B → x ∈ A)))
2		dfcleq 2010	. 2 ⊢ (A = B ↔ ∀x(x ∈ A ↔ x ∈ B))
3		dfss2 2905	. . 3 ⊢ (A ⊆ B ↔ ∀x(x ∈ A → x ∈ B))
4		dfss2 2905	. . 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 1224   = wceq 1226   ∈ wcel 1369   ⊆ wss 2888

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 1312  ax-7 1313  ax-gen 1314  ax-ie1 1358  ax-ie2 1359  ax-8 1371  ax-11 1373  ax-4 1376  ax-17 1395  ax-i9 1399  ax-ial 1403  ax-i5r 1404  ax-ext 1998

This theorem depends on definitions:  df-bi 110  df-nf 1326  df-sb 1622  df-clab 2003  df-cleq 2009  df-clel 2012  df-in 2895  df-ss 2902

This theorem is referenced by:  eqssi  2932  eqssd  2933  sseq1  2937  sseq2  2938  eqimss  2968  ssrabeq  2997  dfpss3  3001  uneqin  3159  ss0b  3227  vss  3235  sssnm  3491  unidif  3578  ssunieq  3579  iuneq1  3636  iuneq2  3639  iunxdif2  3671  ssext  3923  pweqb  3925  eqopab2b  3982  pwunim  3989  soeq2  4019  iunpw  4152  ordunisuc2r  4180  tfi  4223  eqrel  4347  eqrelrel  4359  coeq1  4411  coeq2  4412  cnveq  4427  dmeq  4453  relssres  4566  xp11m  4677  xpcanm  4678  xpcan2m  4679  ssrnres  4681  fnres  4932  eqfnfv3  5183  fneqeql2  5192  fconst4m  5297  f1imaeq  5330  eqoprab2b  5477  fo1stresm  5702  fo2ndresm  5703  nnacan  5987  nnmcan  5994  bj-sseq  8388  bdeq0  8444  bdvsn  8451  bdop  8452  bdeqsuc  8458  bj-om  8513