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

Theorem eqss 3196
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 1600 . 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 2279 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
3 dfss2 3171 . . 3  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
4 dfss2 3171 . . 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 1529    = wceq 1625    e. wcel 1686    C_ wss 3154
This theorem is referenced by:  eqssi  3197  eqssd  3198  sseq1  3201  sseq2  3202  eqimss  3232  dfpss3  3264  uneqin  3422  ss0b  3486  vss  3493  pssdifn0  3517  pwpw0  3765  sssn  3774  ssunsn  3776  pwsnALT  3824  unidif  3861  ssunieq  3862  uniintsn  3901  iuneq1  3920  iuneq2  3923  iunxdif2  3952  ssext  4230  pweqb  4232  eqopab2b  4296  pwun  4304  soeq2  4336  ordtri4  4431  oneqmini  4445  iunpw  4572  orduniorsuc  4623  tfi  4646  eqrel  4779  eqrelrel  4790  coeq1  4843  coeq2  4844  cnveq  4857  dmeq  4881  relssres  4994  xp11  5113  ssrnres  5118  fnres  5362  eqfnfv3  5626  fneqeql2  5636  dff3  5675  fconst4  5738  f1imaeq  5791  eqoprab2b  5908  fo1stres  6145  fo2ndres  6146  tz7.49  6459  oawordeulem  6554  nnacan  6628  nnmcan  6634  ixpeq2  6832  sbthlem3  6975  isinf  7078  ordunifi  7109  inficl  7180  rankr1c  7495  rankc1  7544  iscard  7610  iscard2  7611  carden2  7622  aleph11  7713  cardaleph  7718  alephinit  7724  dfac12a  7776  cflm  7878  cfslb2n  7896  dfacfin7  8027  wrdeq  11426  isumltss  12309  rpnnen2  12506  isprm2  12768  mrcidb2  13522  iscyggen2  15170  iscyg3  15175  lssle0  15709  islpir2  16005  iscss2  16588  ishil2  16621  bastop1  16733  epttop  16748  iscld4  16804  0ntr  16810  opnneiid  16865  isperf2  16885  cnntr  17006  ist1-3  17079  perfcls  17095  cmpfi  17137  iscon2  17142  dfcon2  17147  snfil  17561  filcon  17580  ufileu  17616  alexsubALTlem4  17746  metequiv  18057  shlesb1i  21967  shle0  22023  orthin  22027  chcon2i  22045  chcon3i  22047  chlejb1i  22057  chabs2  22098  h1datomi  22162  cmbr4i  22182  osumcor2i  22225  pjjsi  22281  pjin2i  22775  stcltr2i  22857  mdbr2  22878  dmdbr2  22885  mdsl2i  22904  mdsl2bi  22905  mdslmd3i  22914  chrelat4i  22955  sumdmdlem2  23001  dmdbr5ati  23004  dfon2lem9  24149  wfrlem8  24265  idsset  24432  domfldrefc  25068  ranfldrefc  25069  domintrefb  25074  twsymr  25089  sssu  25152  inposet  25289  dfps2  25300  hdrmp  25717  fneval  26298  equivtotbnd  26513  heiborlem10  26555  isnacs2  26792  mrefg3  26794  pmap11  30024  dia11N  31311  dia2dimlem5  31331  dib11N  31423  dih11  31528  dihglblem6  31603  doch11  31636  mapd11  31902  mapdcnv11N  31922
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-in 3161  df-ss 3168
  Copyright terms: Public domain W3C validator