Theorem eqss 3208

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 1510	. 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 2199	. 2 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
3		ssalel 3181	. . 3 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
4		ssalel 3181	. . 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 1371   = wceq 1373   e. wcel 2176   C_ wss 3166

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-in 3172  df-ss 3179

This theorem is referenced by:  eqssi  3209  eqssd  3210  sseq1  3216  sseq2  3217  eqimss  3247  ssrabeq  3280  uneqin  3424  ss0b  3500  vss  3508  sssnm  3795  unidif  3882  ssunieq  3883  iuneq1  3940  iuneq2  3943  iunxdif2  3976  ssext  4265  pweqb  4267  eqopab2b  4326  pwunim  4333  soeq2  4363  iunpw  4527  ordunisuc2r  4562  tfi  4630  eqrel  4764  eqrelrel  4776  coeq1  4835  coeq2  4836  cnveq  4852  dmeq  4878  relssres  4997  xp11m  5121  xpcanm  5122  xpcan2m  5123  ssrnres  5125  fnres  5392  eqfnfv3  5679  fneqeql2  5689  fconst4m  5804  f1imaeq  5844  eqoprab2b  6003  fo1stresm  6247  fo2ndresm  6248  nnacan  6598  nnmcan  6605  ixpeq2  6799  sbthlemi3  7061  wrdeq  11016  isprm2  12439  lssle0  14134  bastop1  14555  epttop  14562  opnneiid  14636  cnntr  14697  metequiv  14967  bj-sseq  15728  bdeq0  15803  bdvsn  15810  bdop  15811  bdeqsuc  15817  bj-om  15873