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

Theorem eqssi 3457
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 3456 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
41, 2, 3mpbir2an 921 1  |-  A  =  B
Colors of variables: wff setvar class
Syntax hints:    = wceq 1405    C_ wss 3413
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-in 3420  df-ss 3427
This theorem is referenced by:  inv1  3765  unv  3766  intab  4257  intabs  4554  intid  4648  dmv  5038  0ima  5172  fresaunres2  5739  find  6708  dftpos4  6976  wfrlem16  7035  dfom3  8096  tc2  8204  tcidm  8208  tc0  8209  rankuni  8312  rankval4  8316  ackbij1  8649  cfom  8675  fin23lem16  8746  itunitc  8832  inaprc  9243  nqerf  9337  dmrecnq  9375  dmaddsr  9491  dmmulsr  9492  axaddf  9551  axmulf  9552  dfnn2  10588  dfuzi  10993  unirnioo  11676  uzrdgfni  12108  0bits  14296  4sqlem19  14688  ledm  16176  lern  16177  efgsfo  17079  0frgp  17119  indiscld  19883  leordtval2  20004  lecldbas  20011  llyidm  20279  nllyidm  20280  toplly  20281  lly1stc  20287  txuni2  20356  txindis  20425  ust0  21012  qdensere  21567  xrtgioo  21601  zdis  21611  xrhmeo  21736  bndth  21748  ismbf3d  22351  dvef  22671  reeff1o  23132  efifo  23224  dvloglem  23321  logf1o2  23323  choc1  26645  shsidmi  26702  shsval2i  26705  omlsii  26721  chdmm1i  26795  chj1i  26807  chm0i  26808  shjshsi  26810  span0  26860  spanuni  26862  sshhococi  26864  spansni  26875  pjoml4i  26905  pjrni  27020  shatomistici  27679  sumdmdlem2  27737  rinvf1o  27899  sigapildsys  28596  sxbrsigalem0  28705  dya2iocucvr  28718  sxbrsigalem4  28721  sxbrsiga  28724  ballotth  28968  kur14lem6  29495  mrsubrn  29712  msubrn  29728  filnetlem3  30595  filnetlem4  30596  onint1  30668  oninhaus  30669  bj-rabtr  31049  bj-rabtrAUTO  31051  bj-nuliotaALT  31139  icoreunrn  31263  comptiunov2i  35665  compne  36177  unisnALT  36737  fourierdlem62  37300  fouriersw  37363
  Copyright terms: Public domain W3C validator