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

Theorem eqssi 3195
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 3194 . 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 1623    C_ wss 3152
This theorem is referenced by:  inv1  3481  unv  3482  intab  3892  intabs  4172  intid  4231  find  4681  dmv  4894  0ima  5031  fresaunres2  5413  dftpos4  6253  dfom3  7348  tc2  7427  tcidm  7431  tc0  7432  rankuni  7535  rankval4  7539  ackbij1  7864  cfom  7890  fin23lem16  7961  itunitc  8047  inaprc  8458  nqerf  8554  dmrecnq  8592  dmaddsr  8707  dmmulsr  8708  axaddf  8767  axmulf  8768  dfnn2  9759  dfuzi  10102  unirnioo  10743  uzrdgfni  11021  0bits  12630  4sqlem19  13010  ledm  14346  lern  14347  efgsfo  15048  0frgp  15088  indiscld  16828  leordtval2  16942  lecldbas  16949  llyidm  17214  nllyidm  17215  toplly  17216  lly1stc  17222  txuni2  17260  txindis  17328  qdensere  18279  xrtgioo  18312  zdis  18322  xrhmeo  18444  bndth  18456  ismbf3d  19009  dvef  19327  reeff1o  19823  efifo  19909  dvloglem  19995  logf1o2  19997  choc1  21906  shsidmi  21963  shsval2i  21966  omlsii  21982  chdmm1i  22056  chj1i  22068  chm0i  22069  shjshsi  22071  span0  22121  spanuni  22123  sshhococi  22125  spansni  22136  pjoml4i  22166  pjrni  22281  shatomistici  22941  sumdmdlem2  22999  rinvf1o  23038  ballotth  23096  kur14lem6  23742  wfrlem16  24271  onint1  24888  oninhaus  24889  residcp  25077  filnetlem3  26329  filnetlem4  26330  compne  27642  unisnALT  28702
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator