Theorem eqss 2954

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 1373	. 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 2031	. 2 |- (A = B <-> A.x(x e. A <-> x e. B))
3		dfss2 2928	. . 3 |- (A C_ B <-> A.x(x e. A -> x e. B))
4		dfss2 2928	. . 3 |- (B C_ A <-> A.x(x e. B -> x e. A))
5	3, 4	anbi12i 433	. 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 1240   = wceq 1242   e. wcel 1390   C_ wss 2911

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 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-11 1394  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-in 2918  df-ss 2925

This theorem is referenced by:  eqssi  2955  eqssd  2956  sseq1  2960  sseq2  2961  eqimss  2991  ssrabeq  3020  dfpss3  3024  uneqin  3182  ss0b  3250  vss  3258  sssnm  3516  unidif  3603  ssunieq  3604  iuneq1  3661  iuneq2  3664  iunxdif2  3696  ssext  3948  pweqb  3950  eqopab2b  4007  pwunim  4014  soeq2  4044  iunpw  4177  ordunisuc2r  4205  tfi  4248  eqrel  4372  eqrelrel  4384  coeq1  4436  coeq2  4437  cnveq  4452  dmeq  4478  relssres  4591  xp11m  4702  xpcanm  4703  xpcan2m  4704  ssrnres  4706  fnres  4958  eqfnfv3  5210  fneqeql2  5219  fconst4m  5324  f1imaeq  5357  eqoprab2b  5505  fo1stresm  5730  fo2ndresm  5731  nnacan  6021  nnmcan  6028  bj-sseq  9200  bdeq0  9256  bdvsn  9263  bdop  9264  bdeqsuc  9270  bj-om  9325