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

Theorem eqssi 3513
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 3512 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
41, 2, 3mpbir2an 913 1  |-  A  =  B
Colors of variables: wff setvar class
Syntax hints:    = wceq 1374    C_ wss 3469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-in 3476  df-ss 3483
This theorem is referenced by:  inv1  3805  unv  3806  intab  4305  intabs  4601  intid  4698  dmv  5209  0ima  5344  fresaunres2  5748  find  6696  dftpos4  6964  dfom3  8053  tc2  8162  tcidm  8166  tc0  8167  rankuni  8270  rankval4  8274  ackbij1  8607  cfom  8633  fin23lem16  8704  itunitc  8790  inaprc  9203  nqerf  9297  dmrecnq  9335  dmaddsr  9451  dmmulsr  9452  axaddf  9511  axmulf  9512  dfnn2  10538  dfuzi  10940  unirnioo  11613  uzrdgfni  12025  0bits  13937  4sqlem19  14329  ledm  15700  lern  15701  efgsfo  16546  0frgp  16586  indiscld  19351  leordtval2  19472  lecldbas  19479  llyidm  19748  nllyidm  19749  toplly  19750  lly1stc  19756  txuni2  19794  txindis  19863  ust0  20450  qdensere  21005  xrtgioo  21039  zdis  21049  xrhmeo  21174  bndth  21186  ismbf3d  21789  dvef  22109  reeff1o  22569  efifo  22660  dvloglem  22750  logf1o2  22752  choc1  25907  shsidmi  25964  shsval2i  25967  omlsii  25983  chdmm1i  26057  chj1i  26069  chm0i  26070  shjshsi  26072  span0  26122  spanuni  26124  sshhococi  26126  spansni  26137  pjoml4i  26167  pjrni  26282  shatomistici  26942  sumdmdlem2  27000  rinvf1o  27131  sxbrsigalem0  27868  dya2iocucvr  27881  sxbrsigalem4  27884  sxbrsiga  27887  ballotth  28102  kur14lem6  28281  wfrlem16  28921  onint1  29477  oninhaus  29478  filnetlem3  29788  filnetlem4  29789  compne  30882  fourierdlem62  31424  fouriersw  31487  unisnALT  32681  bj-rabtr  33453  bj-rabtrAUTO  33455  bj-nuliotaALT  33543
  Copyright terms: Public domain W3C validator