Metamath Proof Explorer

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 ⊢ ∃! x A F x → F '''' A = ⋃ x | A F x

Proof

Step Hyp Ref Expression
1 eubrv ⊢ ∃! x A F x → A ∈ V
2 euex ⊢ ∃! x A F x → ∃ x A F x
3 eldmg ⊢ A ∈ V → A ∈ dom ⁡ F ↔ ∃ x A F x
4 2 3 syl5ibrcom ⊢ ∃! x A F x → A ∈ V → A ∈ dom ⁡ F
5 4 impcom ⊢ A ∈ V ∧ ∃! x A F x → A ∈ dom ⁡ F
6 dfdfat2 ⊢ F defAt A ↔ A ∈ dom ⁡ F ∧ ∃! x A F x
7 dfatafv2iota ⊢ F defAt A → F '''' A = ι x | A F x
8 iotauni ⊢ ∃! x A F x → ι x | A F x = ⋃ x | A F x
9 7 8 sylan9eq ⊢ F defAt A ∧ ∃! x A F x → F '''' A = ⋃ x | A F x
10 9 ex ⊢ F defAt A → ∃! x A F x → F '''' A = ⋃ x | A F x
11 6 10 sylbir ⊢ A ∈ dom ⁡ F ∧ ∃! x A F x → ∃! x A F x → F '''' A = ⋃ x | A F x
12 11 expcom ⊢ ∃! x A F x → A ∈ dom ⁡ F → ∃! x A F x → F '''' A = ⋃ x | A F x
13 12 pm2.43a ⊢ ∃! x A F x → A ∈ dom ⁡ F → F '''' A = ⋃ x | A F x
14 13 adantl ⊢ A ∈ V ∧ ∃! x A F x → A ∈ dom ⁡ F → F '''' A = ⋃ x | A F x
15 5 14 mpd ⊢ A ∈ V ∧ ∃! x A F x → F '''' A = ⋃ x | A F x
16 1 15 mpancom ⊢ ∃! x A F x → F '''' A = ⋃ x | A F x