Definition df-spr

Description: Define the function which maps a set v to the set of pairs consisting of elements of the set v . (Contributed by AV, 21-Nov-2021)

	Ref	Expression
Assertion	df-spr	⊢ Pairs = ( 𝑣 ∈ V ↦ { 𝑝 ∣ ∃ 𝑎 ∈ 𝑣 ∃ 𝑏 ∈ 𝑣 𝑝 = { 𝑎 , 𝑏 } } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cspr	⊢ Pairs
1		vv	⊢ 𝑣
2		cvv	⊢ V
3		vp	⊢ 𝑝
4		va	⊢ 𝑎
5	1	cv	⊢ 𝑣
6		vb	⊢ 𝑏
7	3	cv	⊢ 𝑝
8	4	cv	⊢ 𝑎
9	6	cv	⊢ 𝑏
10	8 9	cpr	⊢ { 𝑎 , 𝑏 }
11	7 10	wceq	⊢ 𝑝 = { 𝑎 , 𝑏 }
12	11 6 5	wrex	⊢ ∃ 𝑏 ∈ 𝑣 𝑝 = { 𝑎 , 𝑏 }
13	12 4 5	wrex	⊢ ∃ 𝑎 ∈ 𝑣 ∃ 𝑏 ∈ 𝑣 𝑝 = { 𝑎 , 𝑏 }
14	13 3	cab	⊢ { 𝑝 ∣ ∃ 𝑎 ∈ 𝑣 ∃ 𝑏 ∈ 𝑣 𝑝 = { 𝑎 , 𝑏 } }
15	1 2 14	cmpt	⊢ ( 𝑣 ∈ V ↦ { 𝑝 ∣ ∃ 𝑎 ∈ 𝑣 ∃ 𝑏 ∈ 𝑣 𝑝 = { 𝑎 , 𝑏 } } )
16	0 15	wceq	⊢ Pairs = ( 𝑣 ∈ V ↦ { 𝑝 ∣ ∃ 𝑎 ∈ 𝑣 ∃ 𝑏 ∈ 𝑣 𝑝 = { 𝑎 , 𝑏 } } )