Metamath Proof Explorer


Theorem fmptsnd

Description: Express a singleton function in maps-to notation. Deduction form of fmptsng . (Contributed by AV, 4-Aug-2019)

Ref Expression
Hypotheses fmptsnd.1 φ x = A B = C
fmptsnd.2 φ A V
fmptsnd.3 φ C W
Assertion fmptsnd φ A C = x A B

Proof

Step Hyp Ref Expression
1 fmptsnd.1 φ x = A B = C
2 fmptsnd.2 φ A V
3 fmptsnd.3 φ C W
4 velsn x A x = A
5 4 bicomi x = A x A
6 5 anbi1i x = A y = B x A y = B
7 6 opabbii x y | x = A y = B = x y | x A y = B
8 velsn p A C p = A C
9 eqidd φ A = A
10 eqidd φ C = C
11 sbcan [˙C / y]˙ x = A y = B [˙C / y]˙ x = A [˙C / y]˙ y = B
12 sbcg C W [˙C / y]˙ x = A x = A
13 3 12 syl φ [˙C / y]˙ x = A x = A
14 eqsbc3 C W [˙C / y]˙ y = B C = B
15 3 14 syl φ [˙C / y]˙ y = B C = B
16 13 15 anbi12d φ [˙C / y]˙ x = A [˙C / y]˙ y = B x = A C = B
17 11 16 syl5bb φ [˙C / y]˙ x = A y = B x = A C = B
18 17 sbcbidv φ [˙A / x]˙ [˙C / y]˙ x = A y = B [˙A / x]˙ x = A C = B
19 eqeq1 x = A x = A A = A
20 19 adantl φ x = A x = A A = A
21 1 eqeq2d φ x = A C = B C = C
22 20 21 anbi12d φ x = A x = A C = B A = A C = C
23 2 22 sbcied φ [˙A / x]˙ x = A C = B A = A C = C
24 18 23 bitrd φ [˙A / x]˙ [˙C / y]˙ x = A y = B A = A C = C
25 9 10 24 mpbir2and φ [˙A / x]˙ [˙C / y]˙ x = A y = B
26 opelopabsb A C x y | x = A y = B [˙A / x]˙ [˙C / y]˙ x = A y = B
27 25 26 sylibr φ A C x y | x = A y = B
28 eleq1 p = A C p x y | x = A y = B A C x y | x = A y = B
29 27 28 syl5ibrcom φ p = A C p x y | x = A y = B
30 8 29 syl5bi φ p A C p x y | x = A y = B
31 elopab p x y | x = A y = B x y p = x y x = A y = B
32 opeq12 x = A y = B x y = A B
33 32 adantl φ x = A y = B x y = A B
34 33 eqeq2d φ x = A y = B p = x y p = A B
35 1 adantrr φ x = A y = B B = C
36 35 opeq2d φ x = A y = B A B = A C
37 opex A C V
38 37 snid A C A C
39 36 38 eqeltrdi φ x = A y = B A B A C
40 eleq1 p = A B p A C A B A C
41 39 40 syl5ibrcom φ x = A y = B p = A B p A C
42 34 41 sylbid φ x = A y = B p = x y p A C
43 42 ex φ x = A y = B p = x y p A C
44 43 impcomd φ p = x y x = A y = B p A C
45 44 exlimdvv φ x y p = x y x = A y = B p A C
46 31 45 syl5bi φ p x y | x = A y = B p A C
47 30 46 impbid φ p A C p x y | x = A y = B
48 47 eqrdv φ A C = x y | x = A y = B
49 df-mpt x A B = x y | x A y = B
50 49 a1i φ x A B = x y | x A y = B
51 7 48 50 3eqtr4a φ A C = x A B