Metamath Proof Explorer

Theorem 2aryfvalel

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

Ref Expression
Assertion 2aryfvalel 
|- ( X e. V -> ( F e. ( 2 -aryF X ) <-> F : ( X ^m { 0 , 1 } ) --> X ) )

Proof

Step Hyp Ref Expression
1 2nn0 
 |-  2 e. NN0
2 fzo0to2pr 
 |-  ( 0 ..^ 2 ) = { 0 , 1 }
3 2 eqcomi 
 |-  { 0 , 1 } = ( 0 ..^ 2 )
4 3 naryfvalel 
 |-  ( ( 2 e. NN0 /\ X e. V ) -> ( F e. ( 2 -aryF X ) <-> F : ( X ^m { 0 , 1 } ) --> X ) )
5 1 4 mpan 
 |-  ( X e. V -> ( F e. ( 2 -aryF X ) <-> F : ( X ^m { 0 , 1 } ) --> X ) )