Theorem afveu

Description: The value of a function at a unique point, analogous to fveu . (Contributed by Alexander van der Vekens, 29-Nov-2017)

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

Proof

Step	Hyp	Ref	Expression
1		df-br	⊢ ( 𝐴 𝐹 𝑥 ↔ ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐹 )
2	1	eubii	⊢ ( ∃! 𝑥 𝐴 𝐹 𝑥 ↔ ∃! 𝑥 ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐹 )
3		eu2ndop1stv	⊢ ( ∃! 𝑥 ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐹 → 𝐴 ∈ V )
4	2 3	sylbi	⊢ ( ∃! 𝑥 𝐴 𝐹 𝑥 → 𝐴 ∈ V )
5		euex	⊢ ( ∃! 𝑥 𝐴 𝐹 𝑥 → ∃ 𝑥 𝐴 𝐹 𝑥 )
6		eldmg	⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ dom 𝐹 ↔ ∃ 𝑥 𝐴 𝐹 𝑥 ) )
7	5 6	syl5ibrcom	⊢ ( ∃! 𝑥 𝐴 𝐹 𝑥 → ( 𝐴 ∈ V → 𝐴 ∈ dom 𝐹 ) )
8	7	impcom	⊢ ( ( 𝐴 ∈ V ∧ ∃! 𝑥 𝐴 𝐹 𝑥 ) → 𝐴 ∈ dom 𝐹 )
9		dfdfat2	⊢ ( 𝐹 defAt 𝐴 ↔ ( 𝐴 ∈ dom 𝐹 ∧ ∃! 𝑥 𝐴 𝐹 𝑥 ) )
10		afvfundmfveq	⊢ ( 𝐹 defAt 𝐴 → ( 𝐹 ''' 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )
11		fveu	⊢ ( ∃! 𝑥 𝐴 𝐹 𝑥 → ( 𝐹 ‘ 𝐴 ) = ∪ { 𝑥 ∣ 𝐴 𝐹 𝑥 } )
12	10 11	sylan9eq	⊢ ( ( 𝐹 defAt 𝐴 ∧ ∃! 𝑥 𝐴 𝐹 𝑥 ) → ( 𝐹 ''' 𝐴 ) = ∪ { 𝑥 ∣ 𝐴 𝐹 𝑥 } )
13	12	ex	⊢ ( 𝐹 defAt 𝐴 → ( ∃! 𝑥 𝐴 𝐹 𝑥 → ( 𝐹 ''' 𝐴 ) = ∪ { 𝑥 ∣ 𝐴 𝐹 𝑥 } ) )
14	9 13	sylbir	⊢ ( ( 𝐴 ∈ dom 𝐹 ∧ ∃! 𝑥 𝐴 𝐹 𝑥 ) → ( ∃! 𝑥 𝐴 𝐹 𝑥 → ( 𝐹 ''' 𝐴 ) = ∪ { 𝑥 ∣ 𝐴 𝐹 𝑥 } ) )
15	14	expcom	⊢ ( ∃! 𝑥 𝐴 𝐹 𝑥 → ( 𝐴 ∈ dom 𝐹 → ( ∃! 𝑥 𝐴 𝐹 𝑥 → ( 𝐹 ''' 𝐴 ) = ∪ { 𝑥 ∣ 𝐴 𝐹 𝑥 } ) ) )
16	15	pm2.43a	⊢ ( ∃! 𝑥 𝐴 𝐹 𝑥 → ( 𝐴 ∈ dom 𝐹 → ( 𝐹 ''' 𝐴 ) = ∪ { 𝑥 ∣ 𝐴 𝐹 𝑥 } ) )
17	16	adantl	⊢ ( ( 𝐴 ∈ V ∧ ∃! 𝑥 𝐴 𝐹 𝑥 ) → ( 𝐴 ∈ dom 𝐹 → ( 𝐹 ''' 𝐴 ) = ∪ { 𝑥 ∣ 𝐴 𝐹 𝑥 } ) )
18	8 17	mpd	⊢ ( ( 𝐴 ∈ V ∧ ∃! 𝑥 𝐴 𝐹 𝑥 ) → ( 𝐹 ''' 𝐴 ) = ∪ { 𝑥 ∣ 𝐴 𝐹 𝑥 } )
19	4 18	mpancom	⊢ ( ∃! 𝑥 𝐴 𝐹 𝑥 → ( 𝐹 ''' 𝐴 ) = ∪ { 𝑥 ∣ 𝐴 𝐹 𝑥 } )