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

Theorem eqssi 3611
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 3610 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
41, 2, 3mpbir2an 954 1 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1481  wss 3567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-in 3574  df-ss 3581
This theorem is referenced by:  inv1  3961  unv  3962  intab  4498  intabs  4816  intid  4917  dmv  5330  0ima  5470  fresaunres2  6063  find  7076  dftpos4  7356  wfrlem16  7415  dfom3  8529  tc2  8603  tcidm  8607  tc0  8608  rankuni  8711  rankval4  8715  ackbij1  9045  cfom  9071  fin23lem16  9142  itunitc  9228  inaprc  9643  nqerf  9737  dmrecnq  9775  dmaddsr  9891  dmmulsr  9892  axaddf  9951  axmulf  9952  dfnn2  11018  dfuzi  11453  unirnioo  12258  uzrdgfni  12740  0bits  15142  4sqlem19  15648  ledm  17205  lern  17206  efgsfo  18133  0frgp  18173  indiscld  20876  leordtval2  20997  lecldbas  21004  llyidm  21272  nllyidm  21273  toplly  21274  lly1stc  21280  txuni2  21349  txindis  21418  ust0  22004  qdensere  22554  xrtgioo  22590  zdis  22600  xrhmeo  22726  bndth  22738  ismbf3d  23402  dvef  23724  reeff1o  24182  efifo  24274  dvloglem  24375  logf1o2  24377  choc1  28156  shsidmi  28213  shsval2i  28216  omlsii  28232  chdmm1i  28306  chj1i  28318  chm0i  28319  shjshsi  28321  span0  28371  spanuni  28373  sshhococi  28375  spansni  28386  pjoml4i  28416  pjrni  28531  shatomistici  29190  sumdmdlem2  29248  rinvf1o  29405  sigapildsys  30199  sxbrsigalem0  30307  dya2iocucvr  30320  sxbrsigalem4  30323  sxbrsiga  30326  ballotth  30573  kur14lem6  31167  mrsubrn  31384  msubrn  31400  filnetlem3  32350  filnetlem4  32351  onint1  32423  oninhaus  32424  bj-rabtr  32901  bj-rabtrALTALT  32903  bj-rabtrAUTO  32904  bj-disj2r  32988  bj-nuliotaALT  32995  icoreunrn  33178  comptiunov2i  37817  compneOLD  38464  unisnALT  38982  fsumiunss  39607  fourierdlem62  40148  fouriersw  40211  salexct  40315  salgencntex  40324
  Copyright terms: Public domain W3C validator