Theorem eqss 3170

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 1487	. 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 2171	. 2 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
3		dfss2 3144	. . 3 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
4		dfss2 3144	. . 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 1351   = wceq 1353   e. wcel 2148   C_ wss 3129

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3135  df-ss 3142

This theorem is referenced by:  eqssi  3171  eqssd  3172  sseq1  3178  sseq2  3179  eqimss  3209  ssrabeq  3242  uneqin  3386  ss0b  3462  vss  3470  sssnm  3753  unidif  3840  ssunieq  3841  iuneq1  3898  iuneq2  3901  iunxdif2  3933  ssext  4219  pweqb  4221  eqopab2b  4277  pwunim  4284  soeq2  4314  iunpw  4478  ordunisuc2r  4511  tfi  4579  eqrel  4713  eqrelrel  4725  coeq1  4781  coeq2  4782  cnveq  4798  dmeq  4824  relssres  4942  xp11m  5064  xpcanm  5065  xpcan2m  5066  ssrnres  5068  fnres  5329  eqfnfv3  5612  fneqeql2  5622  fconst4m  5733  f1imaeq  5771  eqoprab2b  5928  fo1stresm  6157  fo2ndresm  6158  nnacan  6508  nnmcan  6515  ixpeq2  6707  sbthlemi3  6953  isprm2  12107  bastop1  13365  epttop  13372  opnneiid  13446  cnntr  13507  metequiv  13777  bj-sseq  14315  bdeq0  14390  bdvsn  14397  bdop  14398  bdeqsuc  14404  bj-om  14460