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

Theorem eqssi 3965
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 3964 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
41, 2, 3mpbir2an 710 1 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  wss 3915
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-in 3922  df-ss 3932
This theorem is referenced by:  inv1  4359  unv  4360  intab  4944  intabs  5304  intidOLD  5420  dmv  5883  0ima  6035  cnvrescnv  6152  find  7838  findOLD  7839  dftpos4  8181  wfrlem16OLD  8275  dfom3  9590  dmttrcl  9664  rnttrcl  9665  tc2  9685  tcidm  9689  tc0  9690  rankuni  9806  rankval4  9810  djuunxp  9864  djuun  9869  ackbij1  10181  cfom  10207  fin23lem16  10278  itunitc  10364  inaprc  10779  nqerf  10873  dmrecnq  10911  dmaddsr  11028  dmmulsr  11029  axaddf  11088  axmulf  11089  dfnn2  12173  dfuzi  12601  unirnioo  13373  uzrdgfni  13870  0bits  16326  4sqlem19  16842  ledm  18486  lern  18487  efgsfo  19528  0frgp  19568  indiscld  22458  leordtval2  22579  lecldbas  22586  llyidm  22855  nllyidm  22856  toplly  22857  lly1stc  22863  txuni2  22932  txindis  23001  ust0  23587  qdensere  24149  xrtgioo  24185  zdis  24195  xrhmeo  24325  bndth  24337  ismbf3d  25034  dvef  25360  reeff1o  25822  efifo  25919  dvloglem  26019  logf1o2  26021  bday1s  27192  choc1  30311  shsidmi  30368  shsval2i  30371  omlsii  30387  chdmm1i  30461  chj1i  30473  chm0i  30474  shjshsi  30476  span0  30526  spanuni  30528  sshhococi  30530  spansni  30541  pjoml4i  30571  pjrni  30686  shatomistici  31345  sumdmdlem2  31403  rinvf1o  31586  sigapildsys  32801  sxbrsigalem0  32911  dya2iocucvr  32924  sxbrsigalem4  32927  sxbrsiga  32930  ballotth  33177  kur14lem6  33845  mrsubrn  34147  msubrn  34163  filnetlem3  34881  filnetlem4  34882  onint1  34950  oninhaus  34951  bj-rabtr  35429  bj-rabtrAUTO  35431  bj-disj2r  35528  bj-nuliotaALT  35558  bj-idres  35660  icoreunrn  35859  comptiunov2i  42052  unisnALT  43282  fsumiunss  43890  fourierdlem62  44483  fouriersw  44546  salexct  44649  salgencntex  44658
  Copyright terms: Public domain W3C validator