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

Theorem eqssi 3271
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 3270 . 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 1642    C_ wss 3228
This theorem is referenced by:  inv1  3557  unv  3558  intab  3973  intabs  4253  intid  4313  find  4763  dmv  4976  0ima  5113  fresaunres2  5496  dftpos4  6340  dfom3  7438  tc2  7517  tcidm  7521  tc0  7522  rankuni  7625  rankval4  7629  ackbij1  7954  cfom  7980  fin23lem16  8051  itunitc  8137  inaprc  8548  nqerf  8644  dmrecnq  8682  dmaddsr  8797  dmmulsr  8798  axaddf  8857  axmulf  8858  dfnn2  9849  dfuzi  10194  unirnioo  10835  uzrdgfni  11113  0bits  12727  4sqlem19  13107  ledm  14445  lern  14446  efgsfo  15147  0frgp  15187  indiscld  16934  leordtval2  17048  lecldbas  17055  llyidm  17320  nllyidm  17321  toplly  17322  lly1stc  17328  txuni2  17366  txindis  17434  qdensere  18381  xrtgioo  18414  zdis  18424  xrhmeo  18548  bndth  18560  ismbf3d  19113  dvef  19431  reeff1o  19930  efifo  20016  dvloglem  20106  logf1o2  20108  choc1  22020  shsidmi  22077  shsval2i  22080  omlsii  22096  chdmm1i  22170  chj1i  22182  chm0i  22183  shjshsi  22185  span0  22235  spanuni  22237  sshhococi  22239  spansni  22250  pjoml4i  22280  pjrni  22395  shatomistici  23055  sumdmdlem2  23113  rinvf1o  23246  ust0  23523  sxbrsigalem0  23885  dya2iocucvr  23898  sxbrsigalem4  23901  sxbrsiga  23904  ballotth  24044  kur14lem6  24146  wfrlem16  24829  onint1  25447  oninhaus  25448  filnetlem3  25653  filnetlem4  25654  compne  26965  unisnALT  28464
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-in 3235  df-ss 3242
  Copyright terms: Public domain W3C validator