Metamath Proof Explorer

Theorem fv1prop

Description: The function value of unordered pair of ordered pairs with first components 1 and 2 at 1. (Contributed by AV, 4-Feb-2023)

Ref Expression
Assertion fv1prop 
|- ( A e. V -> ( { <. 1 , A >. , <. 2 , B >. } ` 1 ) = A )

Proof

Step Hyp Ref Expression
1 1ex 
 |-  1 e. _V
2 1ne2 
 |-  1 =/= 2
3 fvpr1g 
 |-  ( ( 1 e. _V /\ A e. V /\ 1 =/= 2 ) -> ( { <. 1 , A >. , <. 2 , B >. } ` 1 ) = A )
4 1 2 3 mp3an13 
 |-  ( A e. V -> ( { <. 1 , A >. , <. 2 , B >. } ` 1 ) = A )