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

Theorem moeq 2680
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 2526 . . . 4 (A V ↔ x x = A)
2 eueq 2676 . . . 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 1873 . 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   = wceq 1219  wex 1350   wcel 1362  ∃!weu 1869  ∃*wmo 1870  Vcvv 2522
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 613  ax-5 1305  ax-7 1306  ax-gen 1307  ax-ie1 1351  ax-ie2 1352  ax-8 1364  ax-10 1365  ax-11 1366  ax-i12 1367  ax-bnd 1368  ax-4 1369  ax-17 1388  ax-i9 1392  ax-ial 1396  ax-i5r 1397  ax-ext 1991
This theorem depends on definitions:  df-bi 110  df-nf 1319  df-sb 1615  df-eu 1872  df-mo 1873  df-clab 1996  df-cleq 2002  df-clel 2005  df-v 2524
This theorem is referenced by:  euxfr2dc  2690  reueq  2702  mosn  3366  sndisj  3719  disjxsn  3721  reusv1  4124  funopabeq  4846  funcnvsn  4855  fvmptg  5157  fvopab6  5173  ovmpt4g  5530  ovi3  5544  ov6g  5545  oprabex3  5663  1stconst  5749  2ndconst  5750
  Copyright terms: Public domain W3C validator