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

Theorem eqssi 3196
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 3195 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
41, 2, 3mpbir2an 886 1  |-  A  =  B
Colors of variables: wff set class
Syntax hints:    = wceq 1623    C_ wss 3153
This theorem is referenced by:  inv1  3482  unv  3483  intab  3893  intabs  4175  intid  4230  find  4680  dmv  4893  0ima  5030  fresaunres2  5379  dftpos4  6215  dfom3  7344  tc2  7423  tcidm  7427  tc0  7428  rankuni  7531  rankval4  7535  ackbij1  7860  cfom  7886  fin23lem16  7957  itunitc  8043  inaprc  8454  nqerf  8550  dmrecnq  8588  dmaddsr  8703  dmmulsr  8704  axaddf  8763  axmulf  8764  dfnn2  9755  dfuzi  10098  unirnioo  10739  uzrdgfni  11017  0bits  12626  4sqlem19  13006  ledm  14342  lern  14343  efgsfo  15044  0frgp  15084  indiscld  16824  leordtval2  16938  lecldbas  16945  llyidm  17210  nllyidm  17211  toplly  17212  lly1stc  17218  txuni2  17256  txindis  17324  qdensere  18275  xrtgioo  18308  zdis  18318  xrhmeo  18440  bndth  18452  ismbf3d  19005  dvef  19323  reeff1o  19819  efifo  19905  dvloglem  19991  logf1o2  19993  choc1  21902  shsidmi  21959  shsval2i  21962  omlsii  21978  chdmm1i  22052  chj1i  22064  chm0i  22065  shjshsi  22067  span0  22117  spanuni  22119  sshhococi  22121  spansni  22132  pjoml4i  22162  pjrni  22277  shatomistici  22937  sumdmdlem2  22995  rinvf1o  23034  ballotth  23092  kur14lem6  23149  wfrlem16  23675  onint1  24298  oninhaus  24299  residcp  24487  filnetlem3  25740  filnetlem4  25741  compne  27053  unisnALT  27982
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 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-in 3160  df-ss 3167
  Copyright terms: Public domain W3C validator