ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  moeq Structured version   GIF version

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

Proof of Theorem moeq
StepHypRef Expression
1 isset 2538 . . . 4 (A V ↔ x x = A)
2 eueq 2688 . . . 4 (A V ↔ ∃!x x = A)
31, 2bitr3i 175 . . 3 (x x = A∃!x x = A)
43biimpi 113 . 2 (x x = A∃!x x = A)
5 df-mo 1886 . 2 (∃*x x = A ↔ (x x = A∃!x x = A))
64, 5mpbir 134 1 ∃*x x = A
Colors of variables: wff set class
Syntax hints:  wi 4  wex 1362   = wceq 1374   wcel 1376  ∃!weu 1882  ∃*wmo 1883  Vcvv 2534
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1378  ax-10 1379  ax-11 1380  ax-i12 1381  ax-bnd 1382  ax-4 1383  ax-17 1402  ax-i9 1406  ax-ial 1411  ax-i5r 1412  ax-ext 2005
This theorem depends on definitions:  df-bi 110  df-nf 1330  df-sb 1629  df-eu 1885  df-mo 1886  df-clab 2010  df-cleq 2016  df-clel 2019  df-v 2536
This theorem is referenced by:  euxfr2dc  2702  reueq  2714  mosn  3359  sndisj  3713  disjxsn  3715  reusv1  4116  funopabeq  4839  funcnvsn  4848  fvmptg  5150  fvopab6  5166  ovmpt4g  5525  ov3  5539  ov6g  5540  oprabex3  5655  1stconst  5741  2ndconst  5742
  Copyright terms: Public domain W3C validator