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

Theorem eqssi 3170
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 3169 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
41, 2, 3mpbir2an 891 1  |-  A  =  B
Colors of variables: wff set class
Syntax hints:    = wceq 1619    C_ wss 3127
This theorem is referenced by:  inv1  3456  unv  3457  intab  3866  intabs  4148  intid  4203  find  4653  dmv  4882  0ima  5019  fresaunres2  5351  dftpos4  6187  dfom3  7316  tc2  7395  tcidm  7399  tc0  7400  rankuni  7503  rankval4  7507  ackbij1  7832  cfom  7858  fin23lem16  7929  itunitc  8015  inaprc  8426  nqerf  8522  dmrecnq  8560  dmaddsr  8675  dmmulsr  8676  axaddf  8735  axmulf  8736  dfnn2  9727  dfuzi  10070  unirnioo  10710  uzrdgfni  10988  0bits  12593  4sqlem19  12973  ledm  14309  lern  14310  efgsfo  15011  0frgp  15051  indiscld  16791  leordtval2  16905  lecldbas  16912  llyidm  17177  nllyidm  17178  toplly  17179  lly1stc  17185  txuni2  17223  txindis  17291  qdensere  18242  xrtgioo  18275  zdis  18285  xrhmeo  18407  bndth  18419  ismbf3d  18972  dvef  19290  reeff1o  19786  efifo  19872  dvloglem  19958  logf1o2  19960  choc1  21867  shsidmi  21924  shsval2i  21927  omlsii  21943  chdmm1i  22017  chj1i  22029  chm0i  22030  shjshsi  22032  span0  22082  spanuni  22084  sshhococi  22086  spansni  22097  pjoml4i  22127  pjrni  22242  shatomistici  22902  sumdmdlem2  22960  rinvf1o  23000  ballotth  23058  kur14lem6  23115  wfrlem16  23641  onint1  24264  oninhaus  24265  residcp  24444  filnetlem3  25697  filnetlem4  25698  compne  27011  unisnALT  27835
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-in 3134  df-ss 3141
  Copyright terms: Public domain W3C validator