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

Theorem eqss 3194
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 1598 . 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 2277 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
3 dfss2 3169 . . 3  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
4 dfss2 3169 . . 3  |-  ( B 
C_  A  <->  A. x
( x  e.  B  ->  x  e.  A ) )
53, 4anbi12i 678 . 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 268 1  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358   A.wal 1527    = wceq 1623    e. wcel 1684    C_ wss 3152
This theorem is referenced by:  eqssi  3195  eqssd  3196  sseq1  3199  sseq2  3200  eqimss  3230  dfpss3  3262  uneqin  3420  ss0b  3484  vss  3491  pssdifn0  3515  pwpw0  3763  sssn  3772  ssunsn  3774  pwsnALT  3822  unidif  3859  ssunieq  3860  uniintsn  3899  iuneq1  3918  iuneq2  3921  iunxdif2  3950  ssext  4228  pweqb  4230  eqopab2b  4294  pwun  4302  soeq2  4334  ordtri4  4429  oneqmini  4443  iunpw  4570  orduniorsuc  4621  tfi  4644  eqrel  4777  eqrelrel  4788  coeq1  4841  coeq2  4842  cnveq  4855  dmeq  4879  relssres  4992  xp11  5111  ssrnres  5116  fnres  5360  eqfnfv3  5624  fneqeql2  5634  dff3  5673  fconst4  5736  f1imaeq  5789  eqoprab2b  5906  fo1stres  6143  fo2ndres  6144  tz7.49  6457  oawordeulem  6552  nnacan  6626  nnmcan  6632  ixpeq2  6830  sbthlem3  6973  isinf  7076  ordunifi  7107  inficl  7178  rankr1c  7493  rankc1  7542  iscard  7608  iscard2  7609  carden2  7620  aleph11  7711  cardaleph  7716  alephinit  7722  dfac12a  7774  cflm  7876  cfslb2n  7894  dfacfin7  8025  wrdeq  11424  isumltss  12307  rpnnen2  12504  isprm2  12766  mrcidb2  13520  iscyggen2  15168  iscyg3  15173  lssle0  15707  islpir2  16003  iscss2  16586  ishil2  16619  bastop1  16731  epttop  16746  iscld4  16802  0ntr  16808  opnneiid  16863  isperf2  16883  cnntr  17004  ist1-3  17077  perfcls  17093  cmpfi  17135  iscon2  17140  dfcon2  17145  snfil  17559  filcon  17578  ufileu  17614  alexsubALTlem4  17744  metequiv  18055  shlesb1i  21965  shle0  22021  orthin  22025  chcon2i  22043  chcon3i  22045  chlejb1i  22055  chabs2  22096  h1datomi  22160  cmbr4i  22180  osumcor2i  22223  pjjsi  22279  pjin2i  22773  stcltr2i  22855  mdbr2  22876  dmdbr2  22883  mdsl2i  22902  mdsl2bi  22903  mdslmd3i  22912  chrelat4i  22953  sumdmdlem2  22999  dmdbr5ati  23002  dfon2lem9  24147  wfrlem8  24263  idsset  24430  domfldrefc  25057  ranfldrefc  25058  domintrefb  25063  twsymr  25078  sssu  25141  inposet  25278  dfps2  25289  hdrmp  25706  fneval  26287  equivtotbnd  26502  heiborlem10  26544  isnacs2  26781  mrefg3  26783  pmap11  29951  dia11N  31238  dia2dimlem5  31258  dib11N  31350  dih11  31455  dihglblem6  31530  doch11  31563  mapd11  31829  mapdcnv11N  31849
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator