Theorem eqss 2936

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 1358	. 2 ⊢ (∀x(x ∈ A ↔ x ∈ B) ↔ (∀x(x ∈ A → x ∈ B) ∧ ∀x(x ∈ B → x ∈ A)))
2		dfcleq 2017	. 2 ⊢ (A = B ↔ ∀x(x ∈ A ↔ x ∈ B))
3		dfss2 2910	. . 3 ⊢ (A ⊆ B ↔ ∀x(x ∈ A → x ∈ B))
4		dfss2 2910	. . 3 ⊢ (B ⊆ A ↔ ∀x(x ∈ B → x ∈ A))
5	3, 4	anbi12i 436	. 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 1226   = wceq 1228   ∈ wcel 1375   ⊆ wss 2893

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 1316  ax-7 1317  ax-gen 1318  ax-ie1 1364  ax-ie2 1365  ax-8 1377  ax-11 1379  ax-4 1382  ax-17 1401  ax-i9 1405  ax-ial 1410  ax-i5r 1411  ax-ext 2005

This theorem depends on definitions:  df-bi 110  df-nf 1330  df-sb 1629  df-clab 2010  df-cleq 2016  df-clel 2019  df-in 2900  df-ss 2907

This theorem is referenced by:  eqssi  2937  eqssd  2938  sseq1  2942  sseq2  2943  eqimss  2973  ssrabeq  3002  dfpss3  3006  uneqin  3164  ss0b  3232  vss  3240  sssnm  3498  unidif  3585  ssunieq  3586  iuneq1  3643  iuneq2  3646  iunxdif2  3678  ssext  3930  pweqb  3932  eqopab2b  3989  pwunim  3996  soeq2  4026  iunpw  4159  ordunisuc2r  4187  tfi  4230  eqrel  4354  eqrelrel  4366  coeq1  4418  coeq2  4419  cnveq  4434  dmeq  4460  relssres  4573  xp11m  4684  xpcanm  4685  xpcan2m  4686  ssrnres  4688  fnres  4939  eqfnfv3  5190  fneqeql2  5199  fconst4m  5304  f1imaeq  5337  eqoprab2b  5484  fo1stresm  5708  fo2ndresm  5709  nnacan  5991  nnmcan  5998  bj-sseq  6387  bdvsn  6447  bdop  6448  bdeq0  6491  bdeqsuc  6492  bj-om  6501  bj-omexALT  6507