Metamath Proof Explorer

Theorem fnsnbg

Description: A function's domain is a singleton iff the function is a singleton. (Contributed by Steven Nguyen, 18-Aug-2023) Relax condition for being in the universal class. (Revised by Zhi Wang, 21-Oct-2025)

Ref Expression
Assertion fnsnbg ⊢ A ∈ V → F Fn A ↔ F = A F ⁡ A

Proof

Step Hyp Ref Expression
1 fnsnr ⊢ F Fn A → x ∈ F → x = A F ⁡ A
2 1 adantl ⊢ A ∈ V ∧ F Fn A → x ∈ F → x = A F ⁡ A
3 fnfun ⊢ F Fn A → Fun ⁡ F
4 snidg ⊢ A ∈ V → A ∈ A
5 4 adantr ⊢ A ∈ V ∧ F Fn A → A ∈ A
6 fndm ⊢ F Fn A → dom ⁡ F = A
7 6 adantl ⊢ A ∈ V ∧ F Fn A → dom ⁡ F = A
8 5 7 eleqtrrd ⊢ A ∈ V ∧ F Fn A → A ∈ dom ⁡ F
9 funfvop ⊢ Fun ⁡ F ∧ A ∈ dom ⁡ F → A F ⁡ A ∈ F
10 3 8 9 syl2an2 ⊢ A ∈ V ∧ F Fn A → A F ⁡ A ∈ F
11 eleq1 ⊢ x = A F ⁡ A → x ∈ F ↔ A F ⁡ A ∈ F
12 10 11 syl5ibrcom ⊢ A ∈ V ∧ F Fn A → x = A F ⁡ A → x ∈ F
13 2 12 impbid ⊢ A ∈ V ∧ F Fn A → x ∈ F ↔ x = A F ⁡ A
14 velsn ⊢ x ∈ A F ⁡ A ↔ x = A F ⁡ A
15 13 14 bitr4di ⊢ A ∈ V ∧ F Fn A → x ∈ F ↔ x ∈ A F ⁡ A
16 15 eqrdv ⊢ A ∈ V ∧ F Fn A → F = A F ⁡ A
17 16 ex ⊢ A ∈ V → F Fn A → F = A F ⁡ A
18 fvex ⊢ F ⁡ A ∈ V
19 fnsng ⊢ A ∈ V ∧ F ⁡ A ∈ V → A F ⁡ A Fn A
20 18 19 mpan2 ⊢ A ∈ V → A F ⁡ A Fn A
21 fneq1 ⊢ F = A F ⁡ A → F Fn A ↔ A F ⁡ A Fn A
22 20 21 syl5ibrcom ⊢ A ∈ V → F = A F ⁡ A → F Fn A
23 17 22 impbid ⊢ A ∈ V → F Fn A ↔ F = A F ⁡ A