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

Theorem eqssi 3477
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 3476 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
41, 2, 3mpbir2an 928 1  |-  A  =  B
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    C_ wss 3433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-in 3440  df-ss 3447
This theorem is referenced by:  inv1  3786  unv  3787  intab  4280  intabs  4578  intid  4672  dmv  5062  0ima  5196  fresaunres2  5764  find  6724  dftpos4  6992  wfrlem16  7051  dfom3  8150  tc2  8223  tcidm  8227  tc0  8228  rankuni  8331  rankval4  8335  ackbij1  8664  cfom  8690  fin23lem16  8761  itunitc  8847  inaprc  9257  nqerf  9351  dmrecnq  9389  dmaddsr  9505  dmmulsr  9506  axaddf  9565  axmulf  9566  dfnn2  10618  dfuzi  11022  unirnioo  11730  uzrdgfni  12165  0bits  14391  4sqlem19  14891  ledm  16448  lern  16449  efgsfo  17367  0frgp  17407  indiscld  20084  leordtval2  20205  lecldbas  20212  llyidm  20480  nllyidm  20481  toplly  20482  lly1stc  20488  txuni2  20557  txindis  20626  ust0  21211  qdensere  21767  xrtgioo  21801  zdis  21811  xrhmeo  21951  bndth  21963  ismbf3d  22587  dvef  22909  reeff1o  23379  efifo  23473  dvloglem  23570  logf1o2  23572  choc1  26956  shsidmi  27013  shsval2i  27016  omlsii  27032  chdmm1i  27106  chj1i  27118  chm0i  27119  shjshsi  27121  span0  27171  spanuni  27173  sshhococi  27175  spansni  27186  pjoml4i  27216  pjrni  27331  shatomistici  27990  sumdmdlem2  28048  rinvf1o  28211  sigapildsys  28973  sxbrsigalem0  29082  dya2iocucvr  29095  sxbrsigalem4  29098  sxbrsiga  29101  ballotth  29359  ballotthOLD  29397  kur14lem6  29923  mrsubrn  30140  msubrn  30156  filnetlem3  31022  filnetlem4  31023  onint1  31095  oninhaus  31096  bj-rabtr  31484  bj-rabtrAUTO  31486  bj-nuliotaALT  31573  icoreunrn  31697  comptiunov2i  36152  compne  36645  unisnALT  37178  fsumiunss  37444  fourierdlem62  37819  fouriersw  37882
  Copyright terms: Public domain W3C validator