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

Theorem eqssi 3356
Description: Infer equality from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 9-Sep-1993.)
Hypotheses
Ref Expression
eqssi.1  |-  A  C_  B
eqssi.2  |-  B  C_  A
Assertion
Ref Expression
eqssi  |-  A  =  B

Proof of Theorem eqssi
StepHypRef Expression
1 eqssi.1 . 2  |-  A  C_  B
2 eqssi.2 . 2  |-  B  C_  A
3 eqss 3355 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
41, 2, 3mpbir2an 887 1  |-  A  =  B
Colors of variables: wff set class
Syntax hints:    = wceq 1652    C_ wss 3312
This theorem is referenced by:  inv1  3646  unv  3647  intab  4072  intabs  4353  intid  4413  find  4862  dmv  5077  0ima  5214  fresaunres2  5607  dftpos4  6490  dfom3  7594  tc2  7673  tcidm  7677  tc0  7678  rankuni  7781  rankval4  7785  ackbij1  8110  cfom  8136  fin23lem16  8207  itunitc  8293  inaprc  8703  nqerf  8799  dmrecnq  8837  dmaddsr  8952  dmmulsr  8953  axaddf  9012  axmulf  9013  dfnn2  10005  dfuzi  10352  unirnioo  10996  uzrdgfni  11290  0bits  12943  4sqlem19  13323  ledm  14661  lern  14662  efgsfo  15363  0frgp  15403  indiscld  17147  leordtval2  17268  lecldbas  17275  llyidm  17543  nllyidm  17544  toplly  17545  lly1stc  17551  txuni2  17589  txindis  17658  ust0  18241  qdensere  18796  xrtgioo  18829  zdis  18839  xrhmeo  18963  bndth  18975  ismbf3d  19538  dvef  19856  reeff1o  20355  efifo  20441  dvloglem  20531  logf1o2  20533  choc1  22821  shsidmi  22878  shsval2i  22881  omlsii  22897  chdmm1i  22971  chj1i  22983  chm0i  22984  shjshsi  22986  span0  23036  spanuni  23038  sshhococi  23040  spansni  23051  pjoml4i  23081  pjrni  23196  shatomistici  23856  sumdmdlem2  23914  rinvf1o  24034  sxbrsigalem0  24613  dya2iocucvr  24626  sxbrsigalem4  24629  sxbrsiga  24632  ballotth  24787  kur14lem6  24889  wfrlem16  25545  onint1  26191  oninhaus  26192  filnetlem3  26400  filnetlem4  26401  compne  27610  unisnALT  28975
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator