Theorem dfafv23

Description: A definition of function value in terms of iota, analogous to dffv3 . (Contributed by AV, 6-Sep-2022)

	Ref	Expression
Assertion	dfafv23	⊢ ( 𝐹 defAt 𝐴 → ( 𝐹 '''' 𝐴 ) = ( ℩ 𝑥 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfatafv2iota	⊢ ( 𝐹 defAt 𝐴 → ( 𝐹 '''' 𝐴 ) = ( ℩ 𝑥 𝐴 𝐹 𝑥 ) )
2		dfdfat2	⊢ ( 𝐹 defAt 𝐴 ↔ ( 𝐴 ∈ dom 𝐹 ∧ ∃! 𝑥 𝐴 𝐹 𝑥 ) )
3	2	simplbi	⊢ ( 𝐹 defAt 𝐴 → 𝐴 ∈ dom 𝐹 )
4		elimasng	⊢ ( ( 𝐴 ∈ dom 𝐹 ∧ 𝑥 ∈ V ) → ( 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) ↔ ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐹 ) )
5	3 4	sylan	⊢ ( ( 𝐹 defAt 𝐴 ∧ 𝑥 ∈ V ) → ( 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) ↔ ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐹 ) )
6		df-br	⊢ ( 𝐴 𝐹 𝑥 ↔ ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐹 )
7	5 6	bitr4di	⊢ ( ( 𝐹 defAt 𝐴 ∧ 𝑥 ∈ V ) → ( 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) ↔ 𝐴 𝐹 𝑥 ) )
8	7	elvd	⊢ ( 𝐹 defAt 𝐴 → ( 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) ↔ 𝐴 𝐹 𝑥 ) )
9	8	iotabidv	⊢ ( 𝐹 defAt 𝐴 → ( ℩ 𝑥 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) ) = ( ℩ 𝑥 𝐴 𝐹 𝑥 ) )
10	1 9	eqtr4d	⊢ ( 𝐹 defAt 𝐴 → ( 𝐹 '''' 𝐴 ) = ( ℩ 𝑥 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) ) )