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

Theorem eqss 3359
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.
StepHypRef Expression
1 albiim 1664 . 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 2427 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
3 dfss2 3333 . . 3  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
4 dfss2 3333 . . 3  |-  ( B 
C_  A  <->  A. x
( x  e.  B  ->  x  e.  A ) )
53, 4anbi12i 690 . 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 277 1  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369   A.wal 1360    = wceq 1362    e. wcel 1755    C_ wss 3316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-in 3323  df-ss 3330
This theorem is referenced by:  eqssi  3360  eqssd  3361  sseq1  3365  sseq2  3366  eqimss  3396  ssrabeq  3426  dfpss3  3430  uneqin  3589  ss0b  3655  vss  3703  pssdifn0  3728  pwpw0  4009  sssn  4019  ssunsn  4021  pwsnALT  4074  unidif  4113  ssunieq  4114  uniintsn  4153  iuneq1  4172  iuneq2  4175  iunxdif2  4206  ssext  4535  pweqb  4537  eqopab2b  4607  pwun  4616  soeq2  4648  ordtri4  4743  oneqmini  4757  eqrel  4916  eqrelrel  4928  coeq1  4984  coeq2  4985  cnveq  5000  dmeq  5027  relssres  5135  xp11  5261  ssrnres  5264  fnres  5515  eqfnfv3  5787  fneqeql2  5800  dff3  5844  fconst4  5929  f1imaeq  5965  eqoprab2b  6133  iunpw  6379  orduniorsuc  6430  tfi  6453  fo1stres  6589  fo2ndres  6590  tz7.49  6886  oawordeulem  6981  nnacan  7055  nnmcan  7061  ixpeq2  7265  sbthlem3  7411  isinf  7514  ordunifi  7550  inficl  7663  rankr1c  8016  rankc1  8065  iscard  8133  iscard2  8134  carden2  8145  aleph11  8242  cardaleph  8247  alephinit  8253  dfac12a  8305  cflm  8407  cfslb2n  8425  dfacfin7  8556  wrdeq  12234  isumltss  13293  rpnnen2  13490  isprm2  13753  mrcidb2  14538  iscyggen2  16337  iscyg3  16342  lssle0  16952  islpir2  17254  iscss2  17952  ishil2  17985  bastop1  18439  epttop  18454  iscld4  18510  0ntr  18516  opnneiid  18571  isperf2  18597  cnntr  18720  ist1-3  18794  perfcls  18810  cmpfi  18852  iscon2  18859  dfcon2  18864  snfil  19278  filcon  19297  ufileu  19333  alexsubALTlem4  19463  metequiv  19925  shlesb1i  24611  shle0  24667  orthin  24671  chcon2i  24689  chcon3i  24691  chlejb1i  24701  chabs2  24742  h1datomi  24806  cmbr4i  24826  osumcor2i  24869  pjjsi  24925  pjin2i  25419  stcltr2i  25501  mdbr2  25522  dmdbr2  25529  mdsl2i  25548  mdsl2bi  25549  mdslmd3i  25558  chrelat4i  25599  sumdmdlem2  25645  dmdbr5ati  25648  eqrelrd2  25769  dfon2lem9  27450  wfrlem8  27577  idsset  27767  fneval  28400  equivtotbnd  28518  heiborlem10  28560  isnacs2  28884  mrefg3  28886  pmap11  32976  dia11N  34263  dia2dimlem5  34283  dib11N  34375  dih11  34480  dihglblem6  34555  doch11  34588  mapd11  34854  mapdcnv11N  34874
  Copyright terms: Public domain W3C validator