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

Definition df-ex 121
Description: Define the existence operator.
Assertion
Ref Expression
df-ex |- T. |= [E. = \p:(al -> *) (A.\q:* [(A.\x:al [(p:(al -> *)x:al) ==> q:*]) ==> q:*])]
Distinct variable group:   p,q,x

Detailed syntax breakdown of Definition df-ex
StepHypRef Expression
1 kt 8 . 2 term T.
2 tex 113 . . 3 term E.
3 hal . . . . 5 type al
4 hb 3 . . . . 5 type *
53, 4ht 2 . . . 4 type (al -> *)
6 vp . . . 4 var p
7 tal 112 . . . . 5 term A.
8 vq . . . . . 6 var q
9 vx . . . . . . . . 9 var x
105, 6tv 1 . . . . . . . . . . 11 term p:(al -> *)
113, 9tv 1 . . . . . . . . . . 11 term x:al
1210, 11kc 5 . . . . . . . . . 10 term (p:(al -> *)x:al)
134, 8tv 1 . . . . . . . . . 10 term q:*
14 tim 111 . . . . . . . . . 10 term ==>
1512, 13, 14kbr 9 . . . . . . . . 9 term [(p:(al -> *)x:al) ==> q:*]
163, 9, 15kl 6 . . . . . . . 8 term \x:al [(p:(al -> *)x:al) ==> q:*]
177, 16kc 5 . . . . . . 7 term (A.\x:al [(p:(al -> *)x:al) ==> q:*])
1817, 13, 14kbr 9 . . . . . 6 term [(A.\x:al [(p:(al -> *)x:al) ==> q:*]) ==> q:*]
194, 8, 18kl 6 . . . . 5 term \q:* [(A.\x:al [(p:(al -> *)x:al) ==> q:*]) ==> q:*]
207, 19kc 5 . . . 4 term (A.\q:* [(A.\x:al [(p:(al -> *)x:al) ==> q:*]) ==> q:*])
215, 6, 20kl 6 . . 3 term \p:(al -> *) (A.\q:* [(A.\x:al [(p:(al -> *)x:al) ==> q:*]) ==> q:*])
22 ke 7 . . 3 term =
232, 21, 22kbr 9 . 2 term [E. = \p:(al -> *) (A.\q:* [(A.\x:al [(p:(al -> *)x:al) ==> q:*]) ==> q:*])]
241, 23wffMMJ2 11 1 wff T. |= [E. = \p:(al -> *) (A.\q:* [(A.\x:al [(p:(al -> *)x:al) ==> q:*]) ==> q:*])]
Colors of variables: type var term
This definition is referenced by:  wex  129  exval  133
  Copyright terms: Public domain W3C validator