Theorem afv2eu

Description: The value of a function at a unique point, analogous to fveu . (Contributed by AV, 5-Sep-2022)

	Ref	Expression
Assertion	afv2eu	⊢ ( ∃! 𝑥 𝐴 𝐹 𝑥 → ( 𝐹 '''' 𝐴 ) = ∪ { 𝑥 ∣ 𝐴 𝐹 𝑥 } )

Proof

Step	Hyp	Ref	Expression
1		eubrv	⊢ ( ∃! 𝑥 𝐴 𝐹 𝑥 → 𝐴 ∈ V )
2		euex	⊢ ( ∃! 𝑥 𝐴 𝐹 𝑥 → ∃ 𝑥 𝐴 𝐹 𝑥 )
3		eldmg	⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ dom 𝐹 ↔ ∃ 𝑥 𝐴 𝐹 𝑥 ) )
4	2 3	syl5ibrcom	⊢ ( ∃! 𝑥 𝐴 𝐹 𝑥 → ( 𝐴 ∈ V → 𝐴 ∈ dom 𝐹 ) )
5	4	impcom	⊢ ( ( 𝐴 ∈ V ∧ ∃! 𝑥 𝐴 𝐹 𝑥 ) → 𝐴 ∈ dom 𝐹 )
6		dfdfat2	⊢ ( 𝐹 defAt 𝐴 ↔ ( 𝐴 ∈ dom 𝐹 ∧ ∃! 𝑥 𝐴 𝐹 𝑥 ) )
7		dfatafv2iota	⊢ ( 𝐹 defAt 𝐴 → ( 𝐹 '''' 𝐴 ) = ( ℩ 𝑥 𝐴 𝐹 𝑥 ) )
8		iotauni	⊢ ( ∃! 𝑥 𝐴 𝐹 𝑥 → ( ℩ 𝑥 𝐴 𝐹 𝑥 ) = ∪ { 𝑥 ∣ 𝐴 𝐹 𝑥 } )
9	7 8	sylan9eq	⊢ ( ( 𝐹 defAt 𝐴 ∧ ∃! 𝑥 𝐴 𝐹 𝑥 ) → ( 𝐹 '''' 𝐴 ) = ∪ { 𝑥 ∣ 𝐴 𝐹 𝑥 } )
10	9	ex	⊢ ( 𝐹 defAt 𝐴 → ( ∃! 𝑥 𝐴 𝐹 𝑥 → ( 𝐹 '''' 𝐴 ) = ∪ { 𝑥 ∣ 𝐴 𝐹 𝑥 } ) )
11	6 10	sylbir	⊢ ( ( 𝐴 ∈ dom 𝐹 ∧ ∃! 𝑥 𝐴 𝐹 𝑥 ) → ( ∃! 𝑥 𝐴 𝐹 𝑥 → ( 𝐹 '''' 𝐴 ) = ∪ { 𝑥 ∣ 𝐴 𝐹 𝑥 } ) )
12	11	expcom	⊢ ( ∃! 𝑥 𝐴 𝐹 𝑥 → ( 𝐴 ∈ dom 𝐹 → ( ∃! 𝑥 𝐴 𝐹 𝑥 → ( 𝐹 '''' 𝐴 ) = ∪ { 𝑥 ∣ 𝐴 𝐹 𝑥 } ) ) )
13	12	pm2.43a	⊢ ( ∃! 𝑥 𝐴 𝐹 𝑥 → ( 𝐴 ∈ dom 𝐹 → ( 𝐹 '''' 𝐴 ) = ∪ { 𝑥 ∣ 𝐴 𝐹 𝑥 } ) )
14	13	adantl	⊢ ( ( 𝐴 ∈ V ∧ ∃! 𝑥 𝐴 𝐹 𝑥 ) → ( 𝐴 ∈ dom 𝐹 → ( 𝐹 '''' 𝐴 ) = ∪ { 𝑥 ∣ 𝐴 𝐹 𝑥 } ) )
15	5 14	mpd	⊢ ( ( 𝐴 ∈ V ∧ ∃! 𝑥 𝐴 𝐹 𝑥 ) → ( 𝐹 '''' 𝐴 ) = ∪ { 𝑥 ∣ 𝐴 𝐹 𝑥 } )
16	1 15	mpancom	⊢ ( ∃! 𝑥 𝐴 𝐹 𝑥 → ( 𝐹 '''' 𝐴 ) = ∪ { 𝑥 ∣ 𝐴 𝐹 𝑥 } )