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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105   A.wal 1400   = wceq 1402   e. wcel 2209   C_ wss 3220

This proof depends on 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 proof 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 used by:  eqssi  3264  eqssd  3265  sseq1  3271  sseq2  3272  eqimss  3302  ssrabeq  3336  uneqin  3482  ss0b  3562  vss  3568  sssnm  3879  unidif  3967  ssunieq  3968  iuneq1  4025  iuneq2  4028  iunxdif2  4061  ssext  4361  pweqb  4363  eqopab2b  4422  pwunim  4431  soeq2  4461  iunpw  4626  ordunisuc2r  4661  tfi  4729  eqrel  4864  eqrelrel  4876  coeq1  4937  coeq2  4938  cnveq  4954  dmeq  4981  relssres  5101  xp11m  5226  xpcanm  5227  xpcan2m  5228  ssrnres  5230  fnres  5500  eqfnfv3  5808  fneqeql2  5818  fconst4m  5935  f1imaeq  5981  eqoprab2b  6146  fo1stresm  6395  fo2ndresm  6396  nnacan  6785  nnmcan  6792  ixpeq2  6994  sbthlemi3  7276  wrdeq  11326  isprm2  12895  lssle0  14709  bastop1  15184  epttop  15191  opnneiid  15265  cnntr  15326  metequiv  15596  bj-sseq  16820  bdeq0  16893  bdvsn  16900  bdop  16901  bdeqsuc  16907  bj-om  16963