Theorem eqss 2937

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 1357	. 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 2016	. 2 |- (A = B <-> A.x(x e. A <-> x e. B))
3		dfss2 2911	. . 3 |- (A C_ B <-> A.x(x e. A -> x e. B))
4		dfss2 2911	. . 3 |- (B C_ A <-> A.x(x e. B -> x e. A))
5	3, 4	anbi12i 436	. 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 201	1 |- (A = B <-> (A C_ B /\ B C_ A))

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98  A.wal 1226   = wceq 1228   e. wcel 1374   C_ wss 2894

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-11 1378  ax-4 1381  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004

This theorem depends on definitions:  df-bi 110  df-nf 1330  df-sb 1628  df-clab 2009  df-cleq 2015  df-clel 2018  df-in 2901  df-ss 2908

This theorem is referenced by:  eqssi  2938  eqssd  2939  sseq1  2943  sseq2  2944  eqimss  2974  ssrabeq  3003  dfpss3  3007  uneqin  3165  ss0b  3233  vss  3241  sssnm  3499  unidif  3586  ssunieq  3587  iuneq1  3644  iuneq2  3647  iunxdif2  3679  ssext  3931  pweqb  3933  eqopab2b  3990  pwunim  3997  soeq2  4027  iunpw  4161  ordunisuc2r  4189  tfi  4232  eqrel  4356  eqrelrel  4368  coeq1  4420  coeq2  4421  cnveq  4436  dmeq  4462  relssres  4575  xp11m  4686  xpcanm  4687  xpcan2m  4688  ssrnres  4690  fnres  4941  eqfnfv3  5192  fneqeql2  5201  fconst4m  5306  f1imaeq  5339  eqoprab2b  5486  fo1stresm  5711  fo2ndresm  5712  nnacan  5996  nnmcan  6003  bj-sseq  7038  bdeq0  7094  bdvsn  7101  bdop  7102  bdeqsuc  7108  bj-om  7159