Theorem eqss 3216

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 1511	. 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 2201	. 2 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
3		ssalel 3189	. . 3 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
4		ssalel 3189	. . 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 2178   C_ wss 3174

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-in 3180  df-ss 3187

This theorem is referenced by:  eqssi  3217  eqssd  3218  sseq1  3224  sseq2  3225  eqimss  3255  ssrabeq  3288  uneqin  3432  ss0b  3508  vss  3516  sssnm  3808  unidif  3896  ssunieq  3897  iuneq1  3954  iuneq2  3957  iunxdif2  3990  ssext  4283  pweqb  4285  eqopab2b  4344  pwunim  4351  soeq2  4381  iunpw  4545  ordunisuc2r  4580  tfi  4648  eqrel  4782  eqrelrel  4794  coeq1  4853  coeq2  4854  cnveq  4870  dmeq  4897  relssres  5016  xp11m  5140  xpcanm  5141  xpcan2m  5142  ssrnres  5144  fnres  5412  eqfnfv3  5702  fneqeql2  5712  fconst4m  5827  f1imaeq  5867  eqoprab2b  6026  fo1stresm  6270  fo2ndresm  6271  nnacan  6621  nnmcan  6628  ixpeq2  6822  sbthlemi3  7087  wrdeq  11053  isprm2  12554  lssle0  14249  bastop1  14670  epttop  14677  opnneiid  14751  cnntr  14812  metequiv  15082  bj-sseq  15928  bdeq0  16002  bdvsn  16009  bdop  16010  bdeqsuc  16016  bj-om  16072