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

Theorem eqssi 3982
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 3981 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
41, 2, 3mpbir2an 709 1 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1533  wss 3935
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3942  df-ss 3951
This theorem is referenced by:  inv1  4347  unv  4348  intab  4905  intabs  5244  intid  5349  dmv  5791  0ima  5945  cnvrescnv  6051  find  7606  dftpos4  7910  wfrlem16  7969  dfom3  9109  tc2  9183  tcidm  9187  tc0  9188  rankuni  9291  rankval4  9295  djuunxp  9349  djuun  9354  ackbij1  9659  cfom  9685  fin23lem16  9756  itunitc  9842  inaprc  10257  nqerf  10351  dmrecnq  10389  dmaddsr  10506  dmmulsr  10507  axaddf  10566  axmulf  10567  dfnn2  11650  dfuzi  12072  unirnioo  12836  uzrdgfni  13325  0bits  15787  4sqlem19  16298  ledm  17833  lern  17834  efgsfo  18864  0frgp  18904  indiscld  21698  leordtval2  21819  lecldbas  21826  llyidm  22095  nllyidm  22096  toplly  22097  lly1stc  22103  txuni2  22172  txindis  22241  ust0  22827  qdensere  23377  xrtgioo  23413  zdis  23423  xrhmeo  23549  bndth  23561  ismbf3d  24254  dvef  24576  reeff1o  25034  efifo  25130  dvloglem  25230  logf1o2  25232  choc1  29103  shsidmi  29160  shsval2i  29163  omlsii  29179  chdmm1i  29253  chj1i  29265  chm0i  29266  shjshsi  29268  span0  29318  spanuni  29320  sshhococi  29322  spansni  29333  pjoml4i  29363  pjrni  29478  shatomistici  30137  sumdmdlem2  30195  rinvf1o  30374  sigapildsys  31421  sxbrsigalem0  31529  dya2iocucvr  31542  sxbrsigalem4  31545  sxbrsiga  31548  ballotth  31795  kur14lem6  32458  mrsubrn  32760  msubrn  32776  filnetlem3  33728  filnetlem4  33729  onint1  33797  oninhaus  33798  bj-rabtr  34248  bj-rabtrAUTO  34250  bj-disj2r  34340  bj-nuliotaALT  34350  bj-idres  34451  icoreunrn  34639  comptiunov2i  40049  unisnALT  41258  fsumiunss  41854  fourierdlem62  42452  fouriersw  42515  salexct  42616  salgencntex  42625
  Copyright terms: Public domain W3C validator