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

Theorem eqssi 3434
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 3433 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
41, 2, 3mpbir2an 934 1  |-  A  =  B
Colors of variables: wff setvar class
Syntax hints:    = wceq 1452    C_ wss 3390
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-in 3397  df-ss 3404
This theorem is referenced by:  inv1  3764  unv  3765  intab  4256  intabs  4562  intid  4658  dmv  5056  0ima  5190  fresaunres2  5767  find  6737  dftpos4  7010  wfrlem16  7069  dfom3  8170  tc2  8244  tcidm  8248  tc0  8249  rankuni  8352  rankval4  8356  ackbij1  8686  cfom  8712  fin23lem16  8783  itunitc  8869  inaprc  9279  nqerf  9373  dmrecnq  9411  dmaddsr  9527  dmmulsr  9528  axaddf  9587  axmulf  9588  dfnn2  10644  dfuzi  11049  unirnioo  11759  uzrdgfni  12210  0bits  14492  4sqlem19  14992  ledm  16548  lern  16549  efgsfo  17467  0frgp  17507  indiscld  20184  leordtval2  20305  lecldbas  20312  llyidm  20580  nllyidm  20581  toplly  20582  lly1stc  20588  txuni2  20657  txindis  20726  ust0  21312  qdensere  21868  xrtgioo  21902  zdis  21912  xrhmeo  22052  bndth  22064  ismbf3d  22689  dvef  23011  reeff1o  23481  efifo  23575  dvloglem  23672  logf1o2  23674  choc1  27061  shsidmi  27118  shsval2i  27121  omlsii  27137  chdmm1i  27211  chj1i  27223  chm0i  27224  shjshsi  27226  span0  27276  spanuni  27278  sshhococi  27280  spansni  27291  pjoml4i  27321  pjrni  27436  shatomistici  28095  sumdmdlem2  28153  rinvf1o  28306  sigapildsys  29058  sxbrsigalem0  29166  dya2iocucvr  29179  sxbrsigalem4  29182  sxbrsiga  29185  ballotth  29443  ballotthOLD  29481  kur14lem6  30006  mrsubrn  30223  msubrn  30239  filnetlem3  31107  filnetlem4  31108  onint1  31180  oninhaus  31181  bj-rabtr  31601  bj-rabtrALTALT  31603  bj-rabtrAUTO  31604  bj-nuliotaALT  31694  icoreunrn  31832  comptiunov2i  36369  compne  36863  unisnALT  37386  fsumiunss  37750  fourierdlem62  38144  fouriersw  38207  salexct  38305  salgencntex  38314
  Copyright terms: Public domain W3C validator