Theorem eqss 3263

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 1540	. 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 2232	. 2 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
3		ssalel 3235	. . 3 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
4		ssalel 3235	. . 3 |- ( B C_ A <-> A. x ( x e. B -> x e. A ) )
5	3, 4	anbi12i 464	. 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 1400   = wceq 1402   e. wcel 2209   C_ wss 3220

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is referenced by:  eqssi  3264  eqssd  3265  sseq1  3271  sseq2  3272  eqimss  3302  ssrabeq  3336  uneqin  3482  ss0b  3562  vss  3567  sssnm  3874  unidif  3962  ssunieq  3963  iuneq1  4020  iuneq2  4023  iunxdif2  4056  ssext  4356  pweqb  4358  eqopab2b  4417  pwunim  4426  soeq2  4456  iunpw  4621  ordunisuc2r  4656  tfi  4724  eqrel  4859  eqrelrel  4871  coeq1  4932  coeq2  4933  cnveq  4949  dmeq  4976  relssres  5096  xp11m  5221  xpcanm  5222  xpcan2m  5223  ssrnres  5225  fnres  5495  eqfnfv3  5799  fneqeql2  5809  fconst4m  5926  f1imaeq  5971  eqoprab2b  6136  fo1stresm  6385  fo2ndresm  6386  nnacan  6775  nnmcan  6782  ixpeq2  6984  sbthlemi3  7266  wrdeq  11304  isprm2  12873  lssle0  14681  bastop1  15107  epttop  15114  opnneiid  15188  cnntr  15249  metequiv  15519  bj-sseq  16734  bdeq0  16807  bdvsn  16814  bdop  16815  bdeqsuc  16821  bj-om  16877