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

Theorem eqssi 3980
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 3979 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
41, 2, 3mpbir2an 707 1 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  wss 3933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-in 3940  df-ss 3949
This theorem is referenced by:  inv1  4345  unv  4346  intab  4897  intabs  5236  intid  5341  dmv  5785  0ima  5939  cnvrescnv  6045  find  7596  dftpos4  7900  wfrlem16  7959  dfom3  9098  tc2  9172  tcidm  9176  tc0  9177  rankuni  9280  rankval4  9284  djuunxp  9338  djuun  9343  ackbij1  9648  cfom  9674  fin23lem16  9745  itunitc  9831  inaprc  10246  nqerf  10340  dmrecnq  10378  dmaddsr  10495  dmmulsr  10496  axaddf  10555  axmulf  10556  dfnn2  11639  dfuzi  12061  unirnioo  12825  uzrdgfni  13314  0bits  15776  4sqlem19  16287  ledm  17822  lern  17823  efgsfo  18794  0frgp  18834  indiscld  21627  leordtval2  21748  lecldbas  21755  llyidm  22024  nllyidm  22025  toplly  22026  lly1stc  22032  txuni2  22101  txindis  22170  ust0  22755  qdensere  23305  xrtgioo  23341  zdis  23351  xrhmeo  23477  bndth  23489  ismbf3d  24182  dvef  24504  reeff1o  24962  efifo  25058  dvloglem  25158  logf1o2  25160  choc1  29031  shsidmi  29088  shsval2i  29091  omlsii  29107  chdmm1i  29181  chj1i  29193  chm0i  29194  shjshsi  29196  span0  29246  spanuni  29248  sshhococi  29250  spansni  29261  pjoml4i  29291  pjrni  29406  shatomistici  30065  sumdmdlem2  30123  rinvf1o  30303  sigapildsys  31320  sxbrsigalem0  31428  dya2iocucvr  31441  sxbrsigalem4  31444  sxbrsiga  31447  ballotth  31694  kur14lem6  32355  mrsubrn  32657  msubrn  32673  filnetlem3  33625  filnetlem4  33626  onint1  33694  oninhaus  33695  bj-rabtr  34145  bj-rabtrAUTO  34147  bj-disj2r  34237  bj-nuliotaALT  34245  bj-idres  34344  icoreunrn  34522  comptiunov2i  39929  unisnALT  41137  fsumiunss  41732  fourierdlem62  42330  fouriersw  42393  salexct  42494  salgencntex  42503
  Copyright terms: Public domain W3C validator