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

Theorem moeq 3275
Description: There is at most one set equal to a class. (Contributed by NM, 8-Mar-1995.)
Assertion
Ref Expression
moeq
Distinct variable group:   ,

Proof of Theorem moeq
StepHypRef Expression
1 isset 3113 . . . 4
2 eueq 3271 . . . 4
31, 2bitr3i 251 . . 3
43biimpi 194 . 2
5 df-mo 2287 . 2
64, 5mpbir 209 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  E.wex 1612  e.wcel 1818  E!weu 2282  E*wmo 2283   cvv 3109
This theorem is referenced by:  mosub  3277  euxfr2  3284  reueq  3297  sndisj  4444  disjxsn  4446  reusv1  4652  reusv2lem1  4653  reuxfr2d  4675  funopabeq  5627  funcnvsn  5638  fvmptg  5954  fvopab6  5980  ovmpt4g  6425  ov3  6439  ov6g  6440  oprabex3  6789  1stconst  6888  2ndconst  6889  iunmapdisj  8425  axaddf  9543  axmulf  9544  joinfval  15631  joinval  15635  meetfval  15645  meetval  15649  reuxfr3d  27388  abrexdom2jm  27406  abrexdom2  30222
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-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-v 3111
  Copyright terms: Public domain W3C validator