df-ofc

Description: Define the function/constant operation map. The definition is designed so that if R is a binary operation, then oFC R is the analogous operation on functions and constants. (Contributed by Thierry Arnoux, 21-Jan-2017)

		Ref	Expression
	Assertion	df-ofc	$⊢ \circ_{fc} R = (f \in V, c \in V ⟼ (x \in dom f ⟼ f (x) R c))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	$class R$
1	0	cofc	$class \circ_{fc} R$
2		vf	$setvar f$
3		cvv	$class V$
4		vc	$setvar c$
5		vx	$setvar x$
6	2	cv	$setvar f$
7	6	cdm	$class dom f$
8	5	cv	$setvar x$
9	8 6	cfv	$class f (x)$
10	4	cv	$setvar c$
11	9 10 0	co	$class (f (x) R c)$
12	5 7 11	cmpt	$class (x \in dom f ⟼ f (x) R c)$
13	2 4 3 3 12	cmpo	$class (f \in V, c \in V ⟼ (x \in dom f ⟼ f (x) R c))$
14	1 13	wceq	$wff \circ_{fc} R = (f \in V, c \in V ⟼ (x \in dom f ⟼ f (x) R c))$

Metamath Proof Explorer

Definition df-ofc

Detailed syntax breakdown