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

Theorem eqssi 3324
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 3323 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
41, 2, 3mpbir2an 887 1  |-  A  =  B
Colors of variables: wff set class
Syntax hints:    = wceq 1649    C_ wss 3280
This theorem is referenced by:  inv1  3614  unv  3615  intab  4040  intabs  4321  intid  4381  find  4829  dmv  5044  0ima  5181  fresaunres2  5574  dftpos4  6457  dfom3  7558  tc2  7637  tcidm  7641  tc0  7642  rankuni  7745  rankval4  7749  ackbij1  8074  cfom  8100  fin23lem16  8171  itunitc  8257  inaprc  8667  nqerf  8763  dmrecnq  8801  dmaddsr  8916  dmmulsr  8917  axaddf  8976  axmulf  8977  dfnn2  9969  dfuzi  10316  unirnioo  10960  uzrdgfni  11253  0bits  12906  4sqlem19  13286  ledm  14624  lern  14625  efgsfo  15326  0frgp  15366  indiscld  17110  leordtval2  17230  lecldbas  17237  llyidm  17504  nllyidm  17505  toplly  17506  lly1stc  17512  txuni2  17550  txindis  17619  ust0  18202  qdensere  18757  xrtgioo  18790  zdis  18800  xrhmeo  18924  bndth  18936  ismbf3d  19499  dvef  19817  reeff1o  20316  efifo  20402  dvloglem  20492  logf1o2  20494  choc1  22782  shsidmi  22839  shsval2i  22842  omlsii  22858  chdmm1i  22932  chj1i  22944  chm0i  22945  shjshsi  22947  span0  22997  spanuni  22999  sshhococi  23001  spansni  23012  pjoml4i  23042  pjrni  23157  shatomistici  23817  sumdmdlem2  23875  rinvf1o  23995  sxbrsigalem0  24574  dya2iocucvr  24587  sxbrsigalem4  24590  sxbrsiga  24593  ballotth  24748  kur14lem6  24850  wfrlem16  25485  onint1  26103  oninhaus  26104  filnetlem3  26299  filnetlem4  26300  compne  27510  unisnALT  28747
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator