HOLE Home Higher-Order Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HOLE Home  >  Th. List  >  df-ex GIF version

Definition df-ex 131
Description: Define the existence operator. (Contributed by Mario Carneiro, 8-Oct-2014.)
Assertion
Ref Expression
df-ex ⊤⊧[ = λp:(α → ∗) (λq:∗ [(λx:α [(p:(α → ∗)x:α) ⇒ q:∗]) ⇒ q:∗])]
Distinct variable group:   p,q,x

Detailed syntax breakdown of Definition df-ex
StepHypRef Expression
1 kt 8 . 2 term
2 tex 123 . . 3 term
3 hal . . . . 5 type α
4 hb 3 . . . . 5 type
53, 4ht 2 . . . 4 type (α → ∗)
6 vp . . . 4 var p
7 tal 122 . . . . 5 term
8 vq . . . . . 6 var q
9 vx . . . . . . . . 9 var x
105, 6tv 1 . . . . . . . . . . 11 term p:(α → ∗)
113, 9tv 1 . . . . . . . . . . 11 term x:α
1210, 11kc 5 . . . . . . . . . 10 term (p:(α → ∗)x:α)
134, 8tv 1 . . . . . . . . . 10 term q:∗
14 tim 121 . . . . . . . . . 10 term
1512, 13, 14kbr 9 . . . . . . . . 9 term [(p:(α → ∗)x:α) ⇒ q:∗]
163, 9, 15kl 6 . . . . . . . 8 term λx:α [(p:(α → ∗)x:α) ⇒ q:∗]
177, 16kc 5 . . . . . . 7 term (λx:α [(p:(α → ∗)x:α) ⇒ q:∗])
1817, 13, 14kbr 9 . . . . . 6 term [(λx:α [(p:(α → ∗)x:α) ⇒ q:∗]) ⇒ q:∗]
194, 8, 18kl 6 . . . . 5 term λq:∗ [(λx:α [(p:(α → ∗)x:α) ⇒ q:∗]) ⇒ q:∗]
207, 19kc 5 . . . 4 term (λq:∗ [(λx:α [(p:(α → ∗)x:α) ⇒ q:∗]) ⇒ q:∗])
215, 6, 20kl 6 . . 3 term λp:(α → ∗) (λq:∗ [(λx:α [(p:(α → ∗)x:α) ⇒ q:∗]) ⇒ q:∗])
22 ke 7 . . 3 term =
232, 21, 22kbr 9 . 2 term [ = λp:(α → ∗) (λq:∗ [(λx:α [(p:(α → ∗)x:α) ⇒ q:∗]) ⇒ q:∗])]
241, 23wffMMJ2 11 1 wff ⊤⊧[ = λp:(α → ∗) (λq:∗ [(λx:α [(p:(α → ∗)x:α) ⇒ q:∗]) ⇒ q:∗])]
Colors of variables: type var term
This definition is referenced by:  wex  139  exval  143
  Copyright terms: Public domain W3C validator