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	⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
Assertion	fmptsng	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → { ⟨ 𝐴 , 𝐶 ⟩ } = ( 𝑥 ∈ { 𝐴 } ↦ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		fmptsng.1	⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
2		velsn	⊢ ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 = 𝐴 )
3	2	bicomi	⊢ ( 𝑥 = 𝐴 ↔ 𝑥 ∈ { 𝐴 } )
4	3	anbi1i	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ↔ ( 𝑥 ∈ { 𝐴 } ∧ 𝑦 = 𝐵 ) )
5	4	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝐴 } ∧ 𝑦 = 𝐵 ) }
6		velsn	⊢ ( 𝑝 ∈ { ⟨ 𝐴 , 𝐶 ⟩ } ↔ 𝑝 = ⟨ 𝐴 , 𝐶 ⟩ )
7		eqidd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → 𝐴 = 𝐴 )
8		eqidd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → 𝐶 = 𝐶 )
9		eqeq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 = 𝐴 ↔ 𝐴 = 𝐴 ) )
10	9	adantr	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐶 ) → ( 𝑥 = 𝐴 ↔ 𝐴 = 𝐴 ) )
11		eqeq1	⊢ ( 𝑦 = 𝐶 → ( 𝑦 = 𝐵 ↔ 𝐶 = 𝐵 ) )
12	1	eqeq2d	⊢ ( 𝑥 = 𝐴 → ( 𝐶 = 𝐵 ↔ 𝐶 = 𝐶 ) )
13	11 12	sylan9bbr	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐶 ) → ( 𝑦 = 𝐵 ↔ 𝐶 = 𝐶 ) )
14	10 13	anbi12d	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐶 ) → ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ↔ ( 𝐴 = 𝐴 ∧ 𝐶 = 𝐶 ) ) )
15	14	opelopabga	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( ⟨ 𝐴 , 𝐶 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) } ↔ ( 𝐴 = 𝐴 ∧ 𝐶 = 𝐶 ) ) )
16	7 8 15	mpbir2and	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ⟨ 𝐴 , 𝐶 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) } )
17		eleq1	⊢ ( 𝑝 = ⟨ 𝐴 , 𝐶 ⟩ → ( 𝑝 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) } ↔ ⟨ 𝐴 , 𝐶 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) } ) )
18	16 17	syl5ibrcom	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝑝 = ⟨ 𝐴 , 𝐶 ⟩ → 𝑝 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) } ) )
19	6 18	syl5bi	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝑝 ∈ { ⟨ 𝐴 , 𝐶 ⟩ } → 𝑝 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) } ) )
20		elopab	⊢ ( 𝑝 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) } ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) )
21		opeq12	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
22	21	eqeq2d	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑝 = ⟨ 𝐴 , 𝐵 ⟩ ) )
23	1	adantr	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝐵 = 𝐶 )
24	23	opeq2d	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝐶 ⟩ )
25		opex	⊢ ⟨ 𝐴 , 𝐶 ⟩ ∈ V
26	25	snid	⊢ ⟨ 𝐴 , 𝐶 ⟩ ∈ { ⟨ 𝐴 , 𝐶 ⟩ }
27	24 26	eqeltrdi	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝐴 , 𝐶 ⟩ } )
28		eleq1	⊢ ( 𝑝 = ⟨ 𝐴 , 𝐵 ⟩ → ( 𝑝 ∈ { ⟨ 𝐴 , 𝐶 ⟩ } ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝐴 , 𝐶 ⟩ } ) )
29	27 28	syl5ibrcom	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑝 = ⟨ 𝐴 , 𝐵 ⟩ → 𝑝 ∈ { ⟨ 𝐴 , 𝐶 ⟩ } ) )
30	22 29	sylbid	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑝 ∈ { ⟨ 𝐴 , 𝐶 ⟩ } ) )
31	30	impcom	⊢ ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → 𝑝 ∈ { ⟨ 𝐴 , 𝐶 ⟩ } )
32	31	exlimivv	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → 𝑝 ∈ { ⟨ 𝐴 , 𝐶 ⟩ } )
33	32	a1i	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( ∃ 𝑥 ∃ 𝑦 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → 𝑝 ∈ { ⟨ 𝐴 , 𝐶 ⟩ } ) )
34	20 33	syl5bi	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝑝 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) } → 𝑝 ∈ { ⟨ 𝐴 , 𝐶 ⟩ } ) )
35	19 34	impbid	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝑝 ∈ { ⟨ 𝐴 , 𝐶 ⟩ } ↔ 𝑝 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) } ) )
36	35	eqrdv	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → { ⟨ 𝐴 , 𝐶 ⟩ } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) } )
37		df-mpt	⊢ ( 𝑥 ∈ { 𝐴 } ↦ 𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝐴 } ∧ 𝑦 = 𝐵 ) }
38	37	a1i	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝑥 ∈ { 𝐴 } ↦ 𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝐴 } ∧ 𝑦 = 𝐵 ) } )
39	5 36 38	3eqtr4a	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → { ⟨ 𝐴 , 𝐶 ⟩ } = ( 𝑥 ∈ { 𝐴 } ↦ 𝐵 ) )