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

Theorem eqssi 3393
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  |-  A  C_  B
eqssi.2  |-  B  C_  A
Assertion
Ref Expression
eqssi  |-  A  =  B

Proof of Theorem eqssi
StepHypRef Expression
1 eqssi.1 . 2  |-  A  C_  B
2 eqssi.2 . 2  |-  B  C_  A
3 eqss 3392 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
41, 2, 3mpbir2an 911 1  |-  A  =  B
Colors of variables: wff setvar class
Syntax hints:    = wceq 1369    C_ wss 3349
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-in 3356  df-ss 3363
This theorem is referenced by:  inv1  3685  unv  3686  intab  4179  intabs  4474  intid  4571  dmv  5076  0ima  5206  fresaunres2  5604  find  6522  dftpos4  6785  dfom3  7874  tc2  7983  tcidm  7987  tc0  7988  rankuni  8091  rankval4  8095  ackbij1  8428  cfom  8454  fin23lem16  8525  itunitc  8611  inaprc  9024  nqerf  9120  dmrecnq  9158  dmaddsr  9273  dmmulsr  9274  axaddf  9333  axmulf  9334  dfnn2  10356  dfuzi  10753  unirnioo  11410  uzrdgfni  11802  0bits  13656  4sqlem19  14045  ledm  15415  lern  15416  efgsfo  16257  0frgp  16297  indiscld  18717  leordtval2  18838  lecldbas  18845  llyidm  19114  nllyidm  19115  toplly  19116  lly1stc  19122  txuni2  19160  txindis  19229  ust0  19816  qdensere  20371  xrtgioo  20405  zdis  20415  xrhmeo  20540  bndth  20552  ismbf3d  21154  dvef  21474  reeff1o  21934  efifo  22025  dvloglem  22115  logf1o2  22117  choc1  24752  shsidmi  24809  shsval2i  24812  omlsii  24828  chdmm1i  24902  chj1i  24914  chm0i  24915  shjshsi  24917  span0  24967  spanuni  24969  sshhococi  24971  spansni  24982  pjoml4i  25012  pjrni  25127  shatomistici  25787  sumdmdlem2  25845  rinvf1o  25971  sxbrsigalem0  26708  dya2iocucvr  26721  sxbrsigalem4  26724  sxbrsiga  26727  ballotth  26942  kur14lem6  27121  wfrlem16  27761  onint1  28317  oninhaus  28318  filnetlem3  28627  filnetlem4  28628  compne  29722  unisnALT  31758  bj-rabtr  32528  bj-rabtrAUTO  32530
  Copyright terms: Public domain W3C validator