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

Theorem eqssi 3208
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 3207 . 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 1632    C_ wss 3165
This theorem is referenced by:  inv1  3494  unv  3495  intab  3908  intabs  4188  intid  4247  find  4697  dmv  4910  0ima  5047  fresaunres2  5429  dftpos4  6269  dfom3  7364  tc2  7443  tcidm  7447  tc0  7448  rankuni  7551  rankval4  7555  ackbij1  7880  cfom  7906  fin23lem16  7977  itunitc  8063  inaprc  8474  nqerf  8570  dmrecnq  8608  dmaddsr  8723  dmmulsr  8724  axaddf  8783  axmulf  8784  dfnn2  9775  dfuzi  10118  unirnioo  10759  uzrdgfni  11037  0bits  12646  4sqlem19  13026  ledm  14362  lern  14363  efgsfo  15064  0frgp  15104  indiscld  16844  leordtval2  16958  lecldbas  16965  llyidm  17230  nllyidm  17231  toplly  17232  lly1stc  17238  txuni2  17276  txindis  17344  qdensere  18295  xrtgioo  18328  zdis  18338  xrhmeo  18460  bndth  18472  ismbf3d  19025  dvef  19343  reeff1o  19839  efifo  19925  dvloglem  20011  logf1o2  20013  choc1  21922  shsidmi  21979  shsval2i  21982  omlsii  21998  chdmm1i  22072  chj1i  22084  chm0i  22085  shjshsi  22087  span0  22137  spanuni  22139  sshhococi  22141  spansni  22152  pjoml4i  22182  pjrni  22297  shatomistici  22957  sumdmdlem2  23015  rinvf1o  23054  ballotth  23112  kur14lem6  23757  wfrlem16  24342  onint1  24960  oninhaus  24961  residcp  25180  filnetlem3  26432  filnetlem4  26433  compne  27745  unisnALT  29018
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator