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  4266  pweqb  4268  eqopab2b  4327  pwunim  4334  soeq2  4364  iunpw  4528  ordunisuc2r  4563  tfi  4631  eqrel  4765  eqrelrel  4777  coeq1  4836  coeq2  4837  cnveq  4853  dmeq  4879  relssres  4998  xp11m  5122  xpcanm  5123  xpcan2m  5124  ssrnres  5126  fnres  5394  eqfnfv3  5681  fneqeql2  5691  fconst4m  5806  f1imaeq  5846  eqoprab2b  6005  fo1stresm  6249  fo2ndresm  6250  nnacan  6600  nnmcan  6607  ixpeq2  6801  sbthlemi3  7063  wrdeq  11018  isprm2  12472  lssle0  14167  bastop1  14588  epttop  14595  opnneiid  14669  cnntr  14730  metequiv  15000  bj-sseq  15765  bdeq0  15840  bdvsn  15847  bdop  15848  bdeqsuc  15854  bj-om  15910