Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  eqssi Unicode version

Theorem eqssi 3120
 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 3119 . 2
41, 2, 3mpbir2an 927 1
 Colors of variables: wff set class Syntax hints:   wceq 1332   wss 3078 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-11 1485  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2123 This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1738  df-clab 2128  df-cleq 2134  df-clel 2137  df-in 3084  df-ss 3091 This theorem is referenced by:  inv1  3406  unv  3407  undifabs  3446  intab  3810  intid  4157  find  4524  limom  4539  dmv  4767  0ima  4911  rnxpid  4985  dftpos4  6172  axaddf  7729  axmulf  7730  dfuzi  9214  unirnioo  9815  txuni2  12500  dvef  12932  reeff1o  12938
 Copyright terms: Public domain W3C validator