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

Theorem eqssi 3137
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 3136 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
41, 2, 3mpbir2an 891 1  |-  A  =  B
Colors of variables: wff set class
Syntax hints:    = wceq 1619    C_ wss 3094
This theorem is referenced by:  inv1  3423  unv  3424  intab  3833  intabs  4114  intid  4169  find  4618  dmv  4847  0ima  4984  fresaunres2  5316  dftpos4  6152  dfom3  7281  tc2  7360  tcidm  7364  tc0  7365  rankuni  7468  rankval4  7472  ackbij1  7797  cfom  7823  fin23lem16  7894  itunitc  7980  inaprc  8391  nqerf  8487  dmrecnq  8525  dmaddsr  8640  dmmulsr  8641  axaddf  8700  axmulf  8701  dfnn2  9692  dfuzi  10034  unirnioo  10674  uzrdgfni  10952  0bits  12557  4sqlem19  12937  ledm  14273  lern  14274  efgsfo  14975  0frgp  15015  indiscld  16755  leordtval2  16869  lecldbas  16876  llyidm  17141  nllyidm  17142  toplly  17143  lly1stc  17149  txuni2  17187  txindis  17255  qdensere  18206  xrtgioo  18239  zdis  18249  xrhmeo  18371  bndth  18383  ismbf3d  18936  dvef  19254  reeff1o  19750  efifo  19836  dvloglem  19922  logf1o2  19924  choc1  21831  shsidmi  21888  shsval2i  21891  omlsii  21907  chdmm1i  21981  chj1i  21993  chm0i  21994  shjshsi  21996  span0  22046  spanuni  22048  sshhococi  22050  spansni  22061  pjoml4i  22109  pjrni  22224  shatomistici  22866  sumdmdlem2  22924  rinvf1o  22964  ballotth  23022  kur14lem6  23079  wfrlem16  23605  onint1  24228  oninhaus  24229  residcp  24408  filnetlem3  25661  filnetlem4  25662  compne  26975  unisnALT  27715
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-in 3101  df-ss 3108
  Copyright terms: Public domain W3C validator