MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqss Structured version   Visualization version   Unicode version

Theorem eqss 3459
Description: The subclass relationship is antisymmetric. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 21-May-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.
StepHypRef Expression
1 albiim 1763 . 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 2456 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
3 dfss2 3433 . . 3  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
4 dfss2 3433 . . 3  |-  ( B 
C_  A  <->  A. x
( x  e.  B  ->  x  e.  A ) )
53, 4anbi12i 708 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  <->  ( A. x ( x  e.  A  ->  x  e.  B )  /\  A. x ( x  e.  B  ->  x  e.  A ) ) )
61, 2, 53bitr4i 285 1  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375   A.wal 1453    = wceq 1455    e. wcel 1898    C_ wss 3416
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-in 3423  df-ss 3430
This theorem is referenced by:  eqssi  3460  eqssd  3461  sseq1  3465  sseq2  3466  eqimss  3496  ssrabeq  3527  dfpss3  3531  uneqin  3706  ss0b  3776  vss  3813  pssdifn0  3839  pwpw0  4133  sssn  4143  ssunsn  4145  pwsnALT  4207  unidif  4245  ssunieq  4246  uniintsn  4286  iuneq1  4306  iuneq2  4309  iunxdif2  4340  ssext  4669  pweqb  4671  eqopab2b  4745  pwun  4761  soeq2  4794  eqrel  4943  eqrelrel  4955  coeq1  5011  coeq2  5012  cnveq  5027  dmeq  5054  relssres  5161  xp11  5291  ssrnres  5294  ordtri4  5479  oneqmini  5493  fnres  5714  eqfnfv3  6001  fneqeql2  6014  dff3  6058  fconst4  6154  f1imaeq  6191  eqoprab2b  6376  iunpw  6632  orduniorsuc  6684  tfi  6707  fo1stres  6844  fo2ndres  6845  wfrlem8  7069  tz7.49  7188  oawordeulem  7281  nnacan  7355  nnmcan  7361  ixpeq2  7562  sbthlem3  7710  isinf  7811  ordunifi  7847  inficl  7965  rankr1c  8318  rankc1  8367  iscard  8435  iscard2  8436  carden2  8447  aleph11  8541  cardaleph  8546  alephinit  8552  dfac12a  8604  cflm  8706  cfslb2n  8724  dfacfin7  8855  wrdeq  12725  isumltss  13955  rpnnen2  14327  isprm2  14681  mrcidb2  15573  iscyggen2  17565  iscyg3  17570  lssle0  18222  islpir2  18524  iscss2  19298  ishil2  19331  bastop1  20058  epttop  20073  iscld4  20130  0ntr  20136  opnneiid  20191  isperf2  20217  cnntr  20340  ist1-3  20414  perfcls  20430  cmpfi  20472  iscon2  20478  dfcon2  20483  snfil  20928  filcon  20947  ufileu  20983  alexsubALTlem4  21114  metequiv  21573  shlesb1i  27088  shle0  27144  orthin  27148  chcon2i  27166  chcon3i  27168  chlejb1i  27178  chabs2  27219  h1datomi  27283  cmbr4i  27303  osumcor2i  27346  pjjsi  27402  pjin2i  27895  stcltr2i  27977  mdbr2  27998  dmdbr2  28005  mdsl2i  28024  mdsl2bi  28025  mdslmd3i  28034  chrelat4i  28075  sumdmdlem2  28121  dmdbr5ati  28124  eqrelrd2  28271  dfon2lem9  30486  idsset  30706  fneval  31057  topdifinfeq  31798  equivtotbnd  32155  heiborlem10  32197  pmap11  33372  dia11N  34661  dia2dimlem5  34681  dib11N  34773  dih11  34878  dihglblem6  34953  doch11  34986  mapd11  35252  mapdcnv11N  35272  isnacs2  35593  mrefg3  35595  rababg  36224  relnonrel  36238  prsal  38217  sssseq  39023  nbuhgr2vtx1edgblem  39469
  Copyright terms: Public domain W3C validator