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	|- ( A = B <-> ( A C_ B /\ B C_ A ) )

Proof of Theorem eqss

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		albiim 1480	. 2 |- ( A. x ( x e. A <-> x e. B ) <-> ( A. x ( x e. A -> x e. B ) /\ A. x ( x e. B -> x e. A ) ) )
2		dfcleq 2164	. 2 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
3		dfss2 3136	. . 3 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
4		dfss2 3136	. . 3 |- ( B C_ A <-> A. x ( x e. B -> x e. A ) )
5	3, 4	anbi12i 457	. 2 |- ( ( A C_ B /\ B C_ A ) <-> ( A. x ( x e. A -> x e. B ) /\ A. x ( x e. B -> x e. A ) ) )
6	1, 2, 5	3bitr4i 211	1 |- ( A = B <-> ( A C_ B /\ B C_ A ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   A.wal 1346   = wceq 1348   e. wcel 2141   C_ 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  3453  vss  3461  sssnm  3739  unidif  3826  ssunieq  3827  iuneq1  3884  iuneq2  3887  iunxdif2  3919  ssext  4204  pweqb  4206  eqopab2b  4262  pwunim  4269  soeq2  4299  iunpw  4463  ordunisuc2r  4496  tfi  4564  eqrel  4698  eqrelrel  4710  coeq1  4766  coeq2  4767  cnveq  4783  dmeq  4809  relssres  4927  xp11m  5047  xpcanm  5048  xpcan2m  5049  ssrnres  5051  fnres  5312  eqfnfv3  5593  fneqeql2  5602  fconst4m  5713  f1imaeq  5751  eqoprab2b  5908  fo1stresm  6137  fo2ndresm  6138  nnacan  6488  nnmcan  6495  ixpeq2  6686  sbthlemi3  6932  isprm2  12058  bastop1  12836  epttop  12843  opnneiid  12917  cnntr  12978  metequiv  13248  bj-sseq  13786  bdeq0  13862  bdvsn  13869  bdop  13870  bdeqsuc  13876  bj-om  13932