Metamath Proof Explorer

Theorem fmptsng

Description: Express a singleton function in maps-to notation. Version of fmptsn allowing the value B to depend on the variable x . (Contributed by AV, 27-Feb-2019)

Ref Expression
Hypothesis fmptsng.1 
|- ( x = A -> B = C )
Assertion fmptsng 
|- ( ( A e. V /\ C e. W ) -> { <. A , C >. } = ( x e. { A } |-> B ) )

Proof

Step Hyp Ref Expression
1 fmptsng.1 
 |-  ( x = A -> B = C )
2 velsn 
 |-  ( x e. { A } <-> x = A )
3 2 bicomi 
 |-  ( x = A <-> x e. { A } )
4 3 anbi1i 
 |-  ( ( x = A /\ y = B ) <-> ( x e. { A } /\ y = B ) )
5 4 opabbii 
 |-  { <. x , y >. | ( x = A /\ y = B ) } = { <. x , y >. | ( x e. { A } /\ y = B ) }
6 velsn 
 |-  ( p e. { <. A , C >. } <-> p = <. A , C >. )
7 eqidd 
 |-  ( ( A e. V /\ C e. W ) -> A = A )
8 eqidd 
 |-  ( ( A e. V /\ C e. W ) -> C = C )
9 eqeq1 
 |-  ( x = A -> ( x = A <-> A = A ) )
10 9 adantr 
 |-  ( ( x = A /\ y = C ) -> ( x = A <-> A = A ) )
11 eqeq1 
 |-  ( y = C -> ( y = B <-> C = B ) )
12 1 eqeq2d 
 |-  ( x = A -> ( C = B <-> C = C ) )
13 11 12 sylan9bbr 
 |-  ( ( x = A /\ y = C ) -> ( y = B <-> C = C ) )
14 10 13 anbi12d 
 |-  ( ( x = A /\ y = C ) -> ( ( x = A /\ y = B ) <-> ( A = A /\ C = C ) ) )
15 14 opelopabga 
 |-  ( ( A e. V /\ C e. W ) -> ( <. A , C >. e. { <. x , y >. | ( x = A /\ y = B ) } <-> ( A = A /\ C = C ) ) )
16 7 8 15 mpbir2and 
 |-  ( ( A e. V /\ C e. W ) -> <. A , C >. e. { <. x , y >. | ( x = A /\ y = B ) } )
17 eleq1 
 |-  ( p = <. A , C >. -> ( p e. { <. x , y >. | ( x = A /\ y = B ) } <-> <. A , C >. e. { <. x , y >. | ( x = A /\ y = B ) } ) )
18 16 17 syl5ibrcom 
 |-  ( ( A e. V /\ C e. W ) -> ( p = <. A , C >. -> p e. { <. x , y >. | ( x = A /\ y = B ) } ) )
19 6 18 syl5bi 
 |-  ( ( A e. V /\ C e. W ) -> ( p e. { <. A , C >. } -> p e. { <. x , y >. | ( x = A /\ y = B ) } ) )
20 elopab 
 |-  ( p e. { <. x , y >. | ( x = A /\ y = B ) } <-> E. x E. y ( p = <. x , y >. /\ ( x = A /\ y = B ) ) )
21 opeq12 
 |-  ( ( x = A /\ y = B ) -> <. x , y >. = <. A , B >. )
22 21 eqeq2d 
 |-  ( ( x = A /\ y = B ) -> ( p = <. x , y >. <-> p = <. A , B >. ) )
23 1 adantr 
 |-  ( ( x = A /\ y = B ) -> B = C )
24 23 opeq2d 
 |-  ( ( x = A /\ y = B ) -> <. A , B >. = <. A , C >. )
25 opex 
 |-  <. A , C >. e. _V
26 25 snid 
 |-  <. A , C >. e. { <. A , C >. }
27 24 26 eqeltrdi 
 |-  ( ( x = A /\ y = B ) -> <. A , B >. e. { <. A , C >. } )
28 eleq1 
 |-  ( p = <. A , B >. -> ( p e. { <. A , C >. } <-> <. A , B >. e. { <. A , C >. } ) )
29 27 28 syl5ibrcom 
 |-  ( ( x = A /\ y = B ) -> ( p = <. A , B >. -> p e. { <. A , C >. } ) )
30 22 29 sylbid 
 |-  ( ( x = A /\ y = B ) -> ( p = <. x , y >. -> p e. { <. A , C >. } ) )
31 30 impcom 
 |-  ( ( p = <. x , y >. /\ ( x = A /\ y = B ) ) -> p e. { <. A , C >. } )
32 31 exlimivv 
 |-  ( E. x E. y ( p = <. x , y >. /\ ( x = A /\ y = B ) ) -> p e. { <. A , C >. } )
33 32 a1i 
 |-  ( ( A e. V /\ C e. W ) -> ( E. x E. y ( p = <. x , y >. /\ ( x = A /\ y = B ) ) -> p e. { <. A , C >. } ) )
34 20 33 syl5bi 
 |-  ( ( A e. V /\ C e. W ) -> ( p e. { <. x , y >. | ( x = A /\ y = B ) } -> p e. { <. A , C >. } ) )
35 19 34 impbid 
 |-  ( ( A e. V /\ C e. W ) -> ( p e. { <. A , C >. } <-> p e. { <. x , y >. | ( x = A /\ y = B ) } ) )
36 35 eqrdv 
 |-  ( ( A e. V /\ C e. W ) -> { <. A , C >. } = { <. x , y >. | ( x = A /\ y = B ) } )
37 df-mpt 
 |-  ( x e. { A } |-> B ) = { <. x , y >. | ( x e. { A } /\ y = B ) }
38 37 a1i 
 |-  ( ( A e. V /\ C e. W ) -> ( x e. { A } |-> B ) = { <. x , y >. | ( x e. { A } /\ y = B ) } )
39 5 36 38 3eqtr4a 
 |-  ( ( A e. V /\ C e. W ) -> { <. A , C >. } = ( x e. { A } |-> B ) )