diff --git a/library/standard/logic/classes/nonempty.lean b/library/standard/logic/classes/nonempty.lean
new file mode 100644
index 000000000..11c0fd5b2
--- /dev/null
+++ b/library/standard/logic/classes/nonempty.lean
@@ -0,0 +1,14 @@
+-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Leonardo de Moura, Jeremy Avigad
+
+import logic.connectives.basic .inhabited
+
+inductive nonempty (A : Type) : Prop :=
+| nonempty_intro : A → nonempty A
+
+definition nonempty_elim {A : Type} {B : Type} (H1 : nonempty A) (H2 : A → B) : B :=
+nonempty_rec H2 H1
+
+theorem inhabited_imp_nonempty [instance] {A : Type} (H : inhabited A) : nonempty A :=
+nonempty_intro (default A)