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

Theorem eqssi 3197
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 3196 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
41, 2, 3mpbir2an 886 1  |-  A  =  B
Colors of variables: wff set class
Syntax hints:    = wceq 1625    C_ wss 3154
This theorem is referenced by:  inv1  3483  unv  3484  intab  3894  intabs  4174  intid  4233  find  4683  dmv  4896  0ima  5033  fresaunres2  5415  dftpos4  6255  dfom3  7350  tc2  7429  tcidm  7433  tc0  7434  rankuni  7537  rankval4  7541  ackbij1  7866  cfom  7892  fin23lem16  7963  itunitc  8049  inaprc  8460  nqerf  8556  dmrecnq  8594  dmaddsr  8709  dmmulsr  8710  axaddf  8769  axmulf  8770  dfnn2  9761  dfuzi  10104  unirnioo  10745  uzrdgfni  11023  0bits  12632  4sqlem19  13012  ledm  14348  lern  14349  efgsfo  15050  0frgp  15090  indiscld  16830  leordtval2  16944  lecldbas  16951  llyidm  17216  nllyidm  17217  toplly  17218  lly1stc  17224  txuni2  17262  txindis  17330  qdensere  18281  xrtgioo  18314  zdis  18324  xrhmeo  18446  bndth  18458  ismbf3d  19011  dvef  19329  reeff1o  19825  efifo  19911  dvloglem  19997  logf1o2  19999  choc1  21908  shsidmi  21965  shsval2i  21968  omlsii  21984  chdmm1i  22058  chj1i  22070  chm0i  22071  shjshsi  22073  span0  22123  spanuni  22125  sshhococi  22127  spansni  22138  pjoml4i  22168  pjrni  22283  shatomistici  22943  sumdmdlem2  23001  rinvf1o  23040  ballotth  23098  kur14lem6  23744  wfrlem16  24273  onint1  24890  oninhaus  24891  residcp  25088  filnetlem3  26340  filnetlem4  26341  compne  27653  unisnALT  28775
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-in 3161  df-ss 3168
  Copyright terms: Public domain W3C validator