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

Theorem eqssi 3579
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 𝐴𝐵
eqssi.2 𝐵𝐴
Assertion
Ref Expression
eqssi 𝐴 = 𝐵

Proof of Theorem eqssi
StepHypRef Expression
1 eqssi.1 . 2 𝐴𝐵
2 eqssi.2 . 2 𝐵𝐴
3 eqss 3578 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
41, 2, 3mpbir2an 956 1 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  wss 3535
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-in 3542  df-ss 3549
This theorem is referenced by:  inv1  3917  unv  3918  intab  4432  intabs  4743  intid  4843  dmv  5245  0ima  5384  fresaunres2  5970  find  6956  dftpos4  7231  wfrlem16  7290  dfom3  8400  tc2  8474  tcidm  8478  tc0  8479  rankuni  8582  rankval4  8586  ackbij1  8916  cfom  8942  fin23lem16  9013  itunitc  9099  inaprc  9510  nqerf  9604  dmrecnq  9642  dmaddsr  9758  dmmulsr  9759  axaddf  9818  axmulf  9819  dfnn2  10876  dfuzi  11296  unirnioo  12096  uzrdgfni  12570  0bits  14941  4sqlem19  15447  ledm  16989  lern  16990  efgsfo  17917  0frgp  17957  indiscld  20643  leordtval2  20764  lecldbas  20771  llyidm  21039  nllyidm  21040  toplly  21041  lly1stc  21047  txuni2  21116  txindis  21185  ust0  21771  qdensere  22311  xrtgioo  22345  zdis  22355  xrhmeo  22480  bndth  22492  ismbf3d  23140  dvef  23460  reeff1o  23918  efifo  24010  dvloglem  24107  logf1o2  24109  choc1  27372  shsidmi  27429  shsval2i  27432  omlsii  27448  chdmm1i  27522  chj1i  27534  chm0i  27535  shjshsi  27537  span0  27587  spanuni  27589  sshhococi  27591  spansni  27602  pjoml4i  27632  pjrni  27747  shatomistici  28406  sumdmdlem2  28464  rinvf1o  28616  sigapildsys  29354  sxbrsigalem0  29462  dya2iocucvr  29475  sxbrsigalem4  29478  sxbrsiga  29481  ballotth  29728  kur14lem6  30249  mrsubrn  30466  msubrn  30482  filnetlem3  31347  filnetlem4  31348  onint1  31420  oninhaus  31421  bj-rabtr  31917  bj-rabtrALTALT  31919  bj-rabtrAUTO  31920  bj-nuliotaALT  32010  icoreunrn  32182  comptiunov2i  36816  compne  37464  unisnALT  37983  fsumiunss  38442  fourierdlem62  38861  fouriersw  38924  salexct  39028  salgencntex  39037
  Copyright terms: Public domain W3C validator