Definition df-ex 131

Description: Define the existence operator. (Contributed by Mario Carneiro, 8-Oct-2014.)

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

Step	Hyp	Ref	Expression
1		kt 8	. 2 term T.
2		tex 123	. . 3 term E.
3		hal	. . . . 5 type al
4		hb 3	. . . . 5 type *
5	3, 4	ht 2	. . . 4 type (al -> *)
6		vp	. . . 4 var p
7		tal 122	. . . . 5 term A.
8		vq	. . . . . 6 var q
9		vx	. . . . . . . . 9 var x
10	5, 6	tv 1	. . . . . . . . . . 11 term p:(al -> *)
11	3, 9	tv 1	. . . . . . . . . . 11 term x:al
12	10, 11	kc 5	. . . . . . . . . 10 term (p:(al -> *)x:al)
13	4, 8	tv 1	. . . . . . . . . 10 term q:*
14		tim 121	. . . . . . . . . 10 term ==>
15	12, 13, 14	kbr 9	. . . . . . . . 9 term [(p:(al -> *)x:al) ==> q:*]
16	3, 9, 15	kl 6	. . . . . . . 8 term \x:al [(p:(al -> *)x:al) ==> q:*]
17	7, 16	kc 5	. . . . . . 7 term (A.\x:al [(p:(al -> *)x:al) ==> q:*])
18	17, 13, 14	kbr 9	. . . . . 6 term [(A.\x:al [(p:(al -> *)x:al) ==> q:*]) ==> q:*]
19	4, 8, 18	kl 6	. . . . 5 term \q:* [(A.\x:al [(p:(al -> *)x:al) ==> q:*]) ==> q:*]
20	7, 19	kc 5	. . . 4 term (A.\q:* [(A.\x:al [(p:(al -> *)x:al) ==> q:*]) ==> q:*])
21	5, 6, 20	kl 6	. . 3 term \p:(al -> *) (A.\q:* [(A.\x:al [(p:(al -> *)x:al) ==> q:*]) ==> q:*])
22		ke 7	. . 3 term =
23	2, 21, 22	kbr 9	. 2 term [E. = \p:(al -> *) (A.\q:* [(A.\x:al [(p:(al -> *)x:al) ==> q:*]) ==> q:*])]
24	1, 23	wffMMJ2 11	1 wff T. |= [E. = \p:(al -> *) (A.\q:* [(A.\x:al [(p:(al -> *)x:al) ==> q:*]) ==> q:*])]

This definition is referenced by:  wex  139  exval  143