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

Theorem eqssi 3116
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 3115 . 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 3078
This theorem is referenced by:  inv1  3388  unv  3389  intab  3790  intabs  4070  intid  4125  find  4572  dmv  4801  0ima  4938  fresaunres2  5270  dftpos4  6105  dfom3  7232  tc2  7311  tcidm  7315  tc0  7316  rankuni  7419  rankval4  7423  ackbij1  7748  cfom  7774  fin23lem16  7845  itunitc  7931  inaprc  8338  nqerf  8434  dmrecnq  8472  dmaddsr  8587  dmmulsr  8588  axaddf  8647  axmulf  8648  dfnn2  9639  dfuzi  9981  unirnioo  10621  uzrdgfni  10899  0bits  12504  4sqlem19  12884  ledm  14181  lern  14182  efgsfo  14883  0frgp  14923  indiscld  16660  leordtval2  16774  lecldbas  16781  llyidm  17046  nllyidm  17047  toplly  17048  lly1stc  17054  txuni2  17092  txindis  17160  qdensere  18111  xrtgioo  18144  zdis  18154  xrhmeo  18276  bndth  18288  ismbf3d  18841  dvef  19159  reeff1o  19655  efifo  19741  dvloglem  19827  logf1o2  19829  choc1  21736  shsidmi  21793  shsval2i  21796  omlsii  21812  chdmm1i  21886  chj1i  21898  chm0i  21899  shjshsi  21901  span0  21951  spanuni  21953  sshhococi  21955  spansni  21966  pjoml4i  22014  pjrni  22129  shatomistici  22771  sumdmdlem2  22829  kur14lem6  22913  wfrlem16  23439  onint1  24062  oninhaus  24063  residcp  24242  filnetlem3  25495  filnetlem4  25496  compne  26809  unisnALT  27489
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 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-in 3085  df-ss 3089
  Copyright terms: Public domain W3C validator