Step |
Hyp |
Ref |
Expression |
1 |
|
c0ex |
|- 0 e. _V |
2 |
|
1ex |
|- 1 e. _V |
3 |
|
simp3 |
|- ( ( A e. V /\ B e. V /\ A =/= B ) -> A =/= B ) |
4 |
|
funcnvpr |
|- ( ( 0 e. _V /\ 1 e. _V /\ A =/= B ) -> Fun `' { <. 0 , A >. , <. 1 , B >. } ) |
5 |
1 2 3 4
|
mp3an12i |
|- ( ( A e. V /\ B e. V /\ A =/= B ) -> Fun `' { <. 0 , A >. , <. 1 , B >. } ) |
6 |
|
s2prop |
|- ( ( A e. V /\ B e. V ) -> <" A B "> = { <. 0 , A >. , <. 1 , B >. } ) |
7 |
6
|
3adant3 |
|- ( ( A e. V /\ B e. V /\ A =/= B ) -> <" A B "> = { <. 0 , A >. , <. 1 , B >. } ) |
8 |
7
|
cnveqd |
|- ( ( A e. V /\ B e. V /\ A =/= B ) -> `' <" A B "> = `' { <. 0 , A >. , <. 1 , B >. } ) |
9 |
8
|
funeqd |
|- ( ( A e. V /\ B e. V /\ A =/= B ) -> ( Fun `' <" A B "> <-> Fun `' { <. 0 , A >. , <. 1 , B >. } ) ) |
10 |
5 9
|
mpbird |
|- ( ( A e. V /\ B e. V /\ A =/= B ) -> Fun `' <" A B "> ) |