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

Theorem eqssi 3505
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 3504 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
41, 2, 3mpbir2an 920 1  |-  A  =  B
Colors of variables: wff setvar class
Syntax hints:    = wceq 1383    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-in 3468  df-ss 3475
This theorem is referenced by:  inv1  3798  unv  3799  intab  4302  intabs  4598  intid  4695  dmv  5208  0ima  5343  fresaunres2  5747  find  6710  dftpos4  6976  dfom3  8067  tc2  8176  tcidm  8180  tc0  8181  rankuni  8284  rankval4  8288  ackbij1  8621  cfom  8647  fin23lem16  8718  itunitc  8804  inaprc  9217  nqerf  9311  dmrecnq  9349  dmaddsr  9465  dmmulsr  9466  axaddf  9525  axmulf  9526  dfnn2  10556  dfuzi  10960  unirnioo  11634  uzrdgfni  12050  0bits  14070  4sqlem19  14462  ledm  15832  lern  15833  efgsfo  16735  0frgp  16775  indiscld  19569  leordtval2  19690  lecldbas  19697  llyidm  19966  nllyidm  19967  toplly  19968  lly1stc  19974  txuni2  20043  txindis  20112  ust0  20699  qdensere  21254  xrtgioo  21288  zdis  21298  xrhmeo  21423  bndth  21435  ismbf3d  22038  dvef  22358  reeff1o  22818  efifo  22910  dvloglem  23005  logf1o2  23007  choc1  26221  shsidmi  26278  shsval2i  26281  omlsii  26297  chdmm1i  26371  chj1i  26383  chm0i  26384  shjshsi  26386  span0  26436  spanuni  26438  sshhococi  26440  spansni  26451  pjoml4i  26481  pjrni  26596  shatomistici  27256  sumdmdlem2  27314  rinvf1o  27448  sxbrsigalem0  28219  dya2iocucvr  28232  sxbrsigalem4  28235  sxbrsiga  28238  ballotth  28453  kur14lem6  28632  mrsubrn  28850  msubrn  28866  wfrlem16  29333  onint1  29889  oninhaus  29890  filnetlem3  30173  filnetlem4  30174  compne  31303  fourierdlem62  31840  fouriersw  31903  unisnALT  33459  bj-rabtr  34245  bj-rabtrAUTO  34247  bj-nuliotaALT  34335
  Copyright terms: Public domain W3C validator