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 ) |
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 ) |