Metamath Proof Explorer

Theorem fv2prop

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 fv2prop 
|- ( B e. V -> ( { <. 1 , A >. , <. 2 , B >. } ` 2 ) = B )

Proof

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