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  4363  pweqb  4365  eqopab2b  4424  pwunim  4433  soeq2  4463  iunpw  4628  ordunisuc2r  4663  tfi  4731  eqrel  4866  eqrelrel  4878  coeq1  4939  coeq2  4940  cnveq  4956  dmeq  4983  relssres  5103  xp11m  5229  xpcanm  5230  xpcan2m  5231  ssrnres  5233  fnres  5503  eqfnfv3  5811  fneqeql2  5821  fconst4m  5938  f1imaeq  5984  eqoprab2b  6149  fo1stresm  6399  fo2ndresm  6400  nnacan  6789  nnmcan  6796  ixpeq2  6998  sbthlemi3  7281  wrdeq  11348  isprm2  12920  lssle0  14818  bastop1  15309  epttop  15316  opnneiid  15390  cnntr  15451  metequiv  15721  bj-sseq  17025  bdeq0  17098  bdvsn  17105  bdop  17106  bdeqsuc  17112  bj-om  17168