Definition df-ov 65

Description: Infix operator. This is a simple metamath way of cleaning up the syntax of all these infix operators to make them a bit more readable than the curried representation.

Hypotheses

Ref	Expression
wov.1	⊢ F:(α → (β → γ))
wov.2	⊢ A:α
wov.3	⊢ B:β

Assertion

Ref	Expression
df-ov	⊢ ⊤⊧(( = [AFB])((FA)B))

Detailed syntax breakdown of Definition df-ov

Step	Hyp	Ref	Expression
1		kt 8	. 2 term ⊤
2		ke 7	. . . 4 term =
3		ta	. . . . 5 term A
4		tb	. . . . 5 term B
5		tf	. . . . 5 term F
6	3, 4, 5	kbr 9	. . . 4 term [AFB]
7	2, 6	kc 5	. . 3 term ( = [AFB])
8	5, 3	kc 5	. . . 4 term (FA)
9	8, 4	kc 5	. . 3 term ((FA)B)
10	7, 9	kc 5	. 2 term (( = [AFB])((FA)B))
11	1, 10	wffMMJ2 11	1 wff ⊤⊧(( = [AFB])((FA)B))

This definition is referenced by:  dfov1  66  dfov2  67  oveq123  88  hbov  101  ovl  107