Definition df-or 132

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

Assertion

Ref	Expression
df-or	|- T. |= [ \/ = \p:* \q:* (A.\x:* [[p:* ==> x:*] ==> [[q:* ==> x:*] ==> x:*]])]

Distinct variable group:   p,q,x

Detailed syntax breakdown of Definition df-or

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

This definition is referenced by:  wor  140  orval  147