Theorem 2aryfvalel

Description: A binary (endo)function on a set X . (Contributed by AV, 20-May-2024)

	Ref	Expression
Assertion	2aryfvalel	⊢ ( 𝑋 ∈ 𝑉 → ( 𝐹 ∈ ( 2 -aryF 𝑋 ) ↔ 𝐹 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		2nn0	⊢ 2 ∈ ℕ0
2		fzo0to2pr	⊢ ( 0 ..^ 2 ) = { 0 , 1 }
3	2	eqcomi	⊢ { 0 , 1 } = ( 0 ..^ 2 )
4	3	naryfvalel	⊢ ( ( 2 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐹 ∈ ( 2 -aryF 𝑋 ) ↔ 𝐹 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ) )
5	1 4	mpan	⊢ ( 𝑋 ∈ 𝑉 → ( 𝐹 ∈ ( 2 -aryF 𝑋 ) ↔ 𝐹 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ) )