Theorem eqss 3242

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 1535	. 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 2225	. 2 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
3		ssalel 3215	. . 3 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
4		ssalel 3215	. . 3 |- ( B C_ A <-> A. x ( x e. B -> x e. A ) )
5	3, 4	anbi12i 460	. 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 212	1 |- ( A = B <-> ( A C_ B /\ B C_ A ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   A.wal 1395   = wceq 1397   e. wcel 2202   C_ wss 3200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  eqssi  3243  eqssd  3244  sseq1  3250  sseq2  3251  eqimss  3281  ssrabeq  3314  uneqin  3458  ss0b  3534  vss  3542  sssnm  3837  unidif  3925  ssunieq  3926  iuneq1  3983  iuneq2  3986  iunxdif2  4019  ssext  4313  pweqb  4315  eqopab2b  4374  pwunim  4383  soeq2  4413  iunpw  4577  ordunisuc2r  4612  tfi  4680  eqrel  4815  eqrelrel  4827  coeq1  4887  coeq2  4888  cnveq  4904  dmeq  4931  relssres  5051  xp11m  5175  xpcanm  5176  xpcan2m  5177  ssrnres  5179  fnres  5449  eqfnfv3  5746  fneqeql2  5756  fconst4m  5873  f1imaeq  5915  eqoprab2b  6078  fo1stresm  6323  fo2ndresm  6324  nnacan  6679  nnmcan  6686  ixpeq2  6880  sbthlemi3  7157  wrdeq  11134  isprm2  12688  lssle0  14385  bastop1  14806  epttop  14813  opnneiid  14887  cnntr  14948  metequiv  15218  bj-sseq  16388  bdeq0  16462  bdvsn  16469  bdop  16470  bdeqsuc  16476  bj-om  16532