Definition df-ptdf 41983

Description: Define the predicate PtDf, which is a utility definition used to shorten definitions and simplify proofs. (Contributed by Andrew Salmon, 15-Jul-2012.)

Assertion

Ref	Expression
df-ptdf	⊢ PtDf(𝐴, 𝐵) = (𝑥 ∈ ℝ ↦ (((𝑥.𝑣(𝐵-𝑟𝐴)) +𝑣 𝐴) “ {1, 2, 3}))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Detailed syntax breakdown of Definition df-ptdf

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3	1, 2	cptdfc 41967	. 2 class PtDf(𝐴, 𝐵)
4		vx	. . 3 setvar 𝑥
5		cr 10801	. . 3 class ℝ
6	4	cv 1538	. . . . . 6 class 𝑥
7		cminusr 41965	. . . . . . 7 class -𝑟
8	2, 1, 7	co 7255	. . . . . 6 class (𝐵-𝑟𝐴)
9		ctimesr 41966	. . . . . 6 class .𝑣
10	6, 8, 9	co 7255	. . . . 5 class (𝑥.𝑣(𝐵-𝑟𝐴))
11		cpv 28848	. . . . 5 class +𝑣
12	10, 1, 11	co 7255	. . . 4 class ((𝑥.𝑣(𝐵-𝑟𝐴)) +𝑣 𝐴)
13		c1 10803	. . . . 5 class 1
14		c2 11958	. . . . 5 class 2
15		c3 11959	. . . . 5 class 3
16	13, 14, 15	ctp 4562	. . . 4 class {1, 2, 3}
17	12, 16	cima 5583	. . 3 class (((𝑥.𝑣(𝐵-𝑟𝐴)) +𝑣 𝐴) “ {1, 2, 3})
18	4, 5, 17	cmpt 5153	. 2 class (𝑥 ∈ ℝ ↦ (((𝑥.𝑣(𝐵-𝑟𝐴)) +𝑣 𝐴) “ {1, 2, 3}))
19	3, 18	wceq 1539	1 wff PtDf(𝐴, 𝐵) = (𝑥 ∈ ℝ ↦ (((𝑥.𝑣(𝐵-𝑟𝐴)) +𝑣 𝐴) “ {1, 2, 3}))

This definition is referenced by: (None)