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

Theorem eqssi 3519
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
eqssi.2
Assertion
Ref Expression
eqssi

Proof of Theorem eqssi
StepHypRef Expression
1 eqssi.1 . 2
2 eqssi.2 . 2
3 eqss 3518 . 2
41, 2, 3mpbir2an 920 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395  C_wss 3475
This theorem is referenced by:  inv1  3812  unv  3813  intab  4317  intabs  4613  intid  4710  dmv  5223  0ima  5358  fresaunres2  5762  find  6725  dftpos4  6993  dfom3  8085  tc2  8194  tcidm  8198  tc0  8199  rankuni  8302  rankval4  8306  ackbij1  8639  cfom  8665  fin23lem16  8736  itunitc  8822  inaprc  9235  nqerf  9329  dmrecnq  9367  dmaddsr  9483  dmmulsr  9484  axaddf  9543  axmulf  9544  dfnn2  10574  dfuzi  10978  unirnioo  11653  uzrdgfni  12069  0bits  14089  4sqlem19  14481  ledm  15854  lern  15855  efgsfo  16757  0frgp  16797  indiscld  19592  leordtval2  19713  lecldbas  19720  llyidm  19989  nllyidm  19990  toplly  19991  lly1stc  19997  txuni2  20066  txindis  20135  ust0  20722  qdensere  21277  xrtgioo  21311  zdis  21321  xrhmeo  21446  bndth  21458  ismbf3d  22061  dvef  22381  reeff1o  22842  efifo  22934  dvloglem  23029  logf1o2  23031  choc1  26245  shsidmi  26302  shsval2i  26305  omlsii  26321  chdmm1i  26395  chj1i  26407  chm0i  26408  shjshsi  26410  span0  26460  spanuni  26462  sshhococi  26464  spansni  26475  pjoml4i  26505  pjrni  26620  shatomistici  27280  sumdmdlem2  27338  rinvf1o  27472  sxbrsigalem0  28242  dya2iocucvr  28255  sxbrsigalem4  28258  sxbrsiga  28261  ballotth  28476  kur14lem6  28655  mrsubrn  28873  msubrn  28889  wfrlem16  29358  onint1  29914  oninhaus  29915  filnetlem3  30198  filnetlem4  30199  compne  31349  fourierdlem62  31951  fouriersw  32014  unisnALT  33726  bj-rabtr  34497  bj-rabtrAUTO  34499  bj-nuliotaALT  34587
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489
  Copyright terms: Public domain W3C validator