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

Theorem moeq 2790
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 2625 . . . 4 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
2 eueq 2786 . . . 4 (𝐴 ∈ V ↔ ∃!𝑥 𝑥 = 𝐴)
31, 2bitr3i 184 . . 3 (∃𝑥 𝑥 = 𝐴 ↔ ∃!𝑥 𝑥 = 𝐴)
43biimpi 118 . 2 (∃𝑥 𝑥 = 𝐴 → ∃!𝑥 𝑥 = 𝐴)
5 df-mo 1952 . 2 (∃*𝑥 𝑥 = 𝐴 ↔ (∃𝑥 𝑥 = 𝐴 → ∃!𝑥 𝑥 = 𝐴))
64, 5mpbir 144 1 ∃*𝑥 𝑥 = 𝐴
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1289  wex 1426  wcel 1438  ∃!weu 1948  ∃*wmo 1949  Vcvv 2619
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-nf 1395  df-sb 1693  df-eu 1951  df-mo 1952  df-clab 2075  df-cleq 2081  df-clel 2084  df-v 2621
This theorem is referenced by:  euxfr2dc  2800  reueq  2814  mosn  3479  sndisj  3841  disjxsn  3843  reusv1  4280  funopabeq  5050  funcnvsn  5059  fvmptg  5380  fvopab6  5396  ovmpt4g  5767  ovi3  5781  ov6g  5782  oprabex3  5900  1stconst  5986  2ndconst  5987
  Copyright terms: Public domain W3C validator