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	$$⊢\left(\phi \wedge x=A\right)\to B=C$$
	fmptsnd.2	$$⊢\phi \to A\in V$$
	fmptsnd.3	$$⊢\phi \to C\in W$$
Assertion	fmptsnd	$$⊢\phi \to \left\{⟨A,C⟩\right\}=\left(x\in \left\{A\right\}⟼B\right)$$

Proof

Step	Hyp	Ref	Expression
1		fmptsnd.1	$$⊢\left(\phi \wedge x=A\right)\to B=C$$
2		fmptsnd.2	$$⊢\phi \to A\in V$$
3		fmptsnd.3	$$⊢\phi \to C\in W$$
4		velsn	$$⊢x\in \left\{A\right\}\leftrightarrow x=A$$
5	4	bicomi	$$⊢x=A\leftrightarrow x\in \left\{A\right\}$$
6	5	anbi1i	$$⊢\left(x=A\wedge y=B\right)\leftrightarrow \left(x\in \left\{A\right\}\wedge y=B\right)$$
7	6	opabbii	$$⊢\left\{⟨x,y⟩|\left(x=A\wedge y=B\right)\right\}=\left\{⟨x,y⟩|\left(x\in \left\{A\right\}\wedge y=B\right)\right\}$$
8		velsn	$$⊢p\in \left\{⟨A,C⟩\right\}\leftrightarrow p=⟨A,C⟩$$
9		eqidd	$$⊢\phi \to A=A$$
10		eqidd	$$⊢\phi \to C=C$$
11		sbcan	$$⊢\underset{\dot{}}{[}C/y\underset{\dot{}}{]}\left(x=A\wedge y=B\right)\leftrightarrow \left(\underset{\dot{}}{[}C/y\underset{\dot{}}{]}x=A\wedge \underset{\dot{}}{[}C/y\underset{\dot{}}{]}y=B\right)$$
12		sbcg	$$⊢C\in W\to \left(\underset{\dot{}}{[}C/y\underset{\dot{}}{]}x=A\leftrightarrow x=A\right)$$
13	3 12	syl	$$⊢\phi \to \left(\underset{\dot{}}{[}C/y\underset{\dot{}}{]}x=A\leftrightarrow x=A\right)$$
14		eqsbc1	$$⊢C\in W\to \left(\underset{\dot{}}{[}C/y\underset{\dot{}}{]}y=B\leftrightarrow C=B\right)$$
15	3 14	syl	$$⊢\phi \to \left(\underset{\dot{}}{[}C/y\underset{\dot{}}{]}y=B\leftrightarrow C=B\right)$$
16	13 15	anbi12d	$$⊢\phi \to \left(\left(\underset{\dot{}}{[}C/y\underset{\dot{}}{]}x=A\wedge \underset{\dot{}}{[}C/y\underset{\dot{}}{]}y=B\right)\leftrightarrow \left(x=A\wedge C=B\right)\right)$$
17	11 16	bitrid	$$⊢\phi \to \left(\underset{\dot{}}{[}C/y\underset{\dot{}}{]}\left(x=A\wedge y=B\right)\leftrightarrow \left(x=A\wedge C=B\right)\right)$$
18	17	sbcbidv	$$⊢\phi \to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}C/y\underset{\dot{}}{]}\left(x=A\wedge y=B\right)\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(x=A\wedge C=B\right)\right)$$
19		eqeq1	$$⊢x=A\to \left(x=A\leftrightarrow A=A\right)$$
20	19	adantl	$$⊢\left(\phi \wedge x=A\right)\to \left(x=A\leftrightarrow A=A\right)$$
21	1	eqeq2d	$$⊢\left(\phi \wedge x=A\right)\to \left(C=B\leftrightarrow C=C\right)$$
22	20 21	anbi12d	$$⊢\left(\phi \wedge x=A\right)\to \left(\left(x=A\wedge C=B\right)\leftrightarrow \left(A=A\wedge C=C\right)\right)$$
23	2 22	sbcied	$$⊢\phi \to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(x=A\wedge C=B\right)\leftrightarrow \left(A=A\wedge C=C\right)\right)$$
24	18 23	bitrd	$$⊢\phi \to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}C/y\underset{\dot{}}{]}\left(x=A\wedge y=B\right)\leftrightarrow \left(A=A\wedge C=C\right)\right)$$
25	9 10 24	mpbir2and	$$⊢\phi \to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}C/y\underset{\dot{}}{]}\left(x=A\wedge y=B\right)$$
26		opelopabsb	$$⊢⟨A,C⟩\in \left\{⟨x,y⟩|\left(x=A\wedge y=B\right)\right\}\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}C/y\underset{\dot{}}{]}\left(x=A\wedge y=B\right)$$
27	25 26	sylibr	$$⊢\phi \to ⟨A,C⟩\in \left\{⟨x,y⟩|\left(x=A\wedge y=B\right)\right\}$$
28		eleq1	$$⊢p=⟨A,C⟩\to \left(p\in \left\{⟨x,y⟩|\left(x=A\wedge y=B\right)\right\}\leftrightarrow ⟨A,C⟩\in \left\{⟨x,y⟩|\left(x=A\wedge y=B\right)\right\}\right)$$
29	27 28	syl5ibrcom	$$⊢\phi \to \left(p=⟨A,C⟩\to p\in \left\{⟨x,y⟩|\left(x=A\wedge y=B\right)\right\}\right)$$
30	8 29	syl5bi	$$⊢\phi \to \left(p\in \left\{⟨A,C⟩\right\}\to p\in \left\{⟨x,y⟩|\left(x=A\wedge y=B\right)\right\}\right)$$
31		elopab	$$⊢p\in \left\{⟨x,y⟩|\left(x=A\wedge y=B\right)\right\}\leftrightarrow \exists x\exists y\left(p=⟨x,y⟩\wedge \left(x=A\wedge y=B\right)\right)$$
32		opeq12	$$⊢\left(x=A\wedge y=B\right)\to ⟨x,y⟩=⟨A,B⟩$$
33	32	adantl	$$⊢\left(\phi \wedge \left(x=A\wedge y=B\right)\right)\to ⟨x,y⟩=⟨A,B⟩$$
34	33	eqeq2d	$$⊢\left(\phi \wedge \left(x=A\wedge y=B\right)\right)\to \left(p=⟨x,y⟩\leftrightarrow p=⟨A,B⟩\right)$$
35	1	adantrr	$$⊢\left(\phi \wedge \left(x=A\wedge y=B\right)\right)\to B=C$$
36	35	opeq2d	$$⊢\left(\phi \wedge \left(x=A\wedge y=B\right)\right)\to ⟨A,B⟩=⟨A,C⟩$$
37		opex	$$⊢⟨A,C⟩\in \mathrm{V}$$
38	37	snid	$$⊢⟨A,C⟩\in \left\{⟨A,C⟩\right\}$$
39	36 38	eqeltrdi	$$⊢\left(\phi \wedge \left(x=A\wedge y=B\right)\right)\to ⟨A,B⟩\in \left\{⟨A,C⟩\right\}$$
40		eleq1	$$⊢p=⟨A,B⟩\to \left(p\in \left\{⟨A,C⟩\right\}\leftrightarrow ⟨A,B⟩\in \left\{⟨A,C⟩\right\}\right)$$
41	39 40	syl5ibrcom	$$⊢\left(\phi \wedge \left(x=A\wedge y=B\right)\right)\to \left(p=⟨A,B⟩\to p\in \left\{⟨A,C⟩\right\}\right)$$
42	34 41	sylbid	$$⊢\left(\phi \wedge \left(x=A\wedge y=B\right)\right)\to \left(p=⟨x,y⟩\to p\in \left\{⟨A,C⟩\right\}\right)$$
43	42	ex	$$⊢\phi \to \left(\left(x=A\wedge y=B\right)\to \left(p=⟨x,y⟩\to p\in \left\{⟨A,C⟩\right\}\right)\right)$$
44	43	impcomd	$$⊢\phi \to \left(\left(p=⟨x,y⟩\wedge \left(x=A\wedge y=B\right)\right)\to p\in \left\{⟨A,C⟩\right\}\right)$$
45	44	exlimdvv	$$⊢\phi \to \left(\exists x\exists y\left(p=⟨x,y⟩\wedge \left(x=A\wedge y=B\right)\right)\to p\in \left\{⟨A,C⟩\right\}\right)$$
46	31 45	syl5bi	$$⊢\phi \to \left(p\in \left\{⟨x,y⟩|\left(x=A\wedge y=B\right)\right\}\to p\in \left\{⟨A,C⟩\right\}\right)$$
47	30 46	impbid	$$⊢\phi \to \left(p\in \left\{⟨A,C⟩\right\}\leftrightarrow p\in \left\{⟨x,y⟩|\left(x=A\wedge y=B\right)\right\}\right)$$
48	47	eqrdv	$$⊢\phi \to \left\{⟨A,C⟩\right\}=\left\{⟨x,y⟩|\left(x=A\wedge y=B\right)\right\}$$
49		df-mpt	$$⊢\left(x\in \left\{A\right\}⟼B\right)=\left\{⟨x,y⟩|\left(x\in \left\{A\right\}\wedge y=B\right)\right\}$$
50	49	a1i	$$⊢\phi \to \left(x\in \left\{A\right\}⟼B\right)=\left\{⟨x,y⟩|\left(x\in \left\{A\right\}\wedge y=B\right)\right\}$$
51	7 48 50	3eqtr4a	$$⊢\phi \to \left\{⟨A,C⟩\right\}=\left(x\in \left\{A\right\}⟼B\right)$$