Metamath Proof Explorer


Theorem f1cdmsn

Description: If a one-to-one function with a nonempty domain has a singleton as its codomain, its domain must also be a singleton. (Contributed by BTernaryTau, 1-Dec-2024)

Ref Expression
Assertion f1cdmsn F : A 1-1 B A x A = x

Proof

Step Hyp Ref Expression
1 f1f F : A 1-1 B F : A B
2 fvconst F : A B y A F y = B
3 2 3adant3 F : A B y A z A F y = B
4 fvconst F : A B z A F z = B
5 4 3adant2 F : A B y A z A F z = B
6 3 5 eqtr4d F : A B y A z A F y = F z
7 1 6 syl3an1 F : A 1-1 B y A z A F y = F z
8 f1veqaeq F : A 1-1 B y A z A F y = F z y = z
9 8 3impb F : A 1-1 B y A z A F y = F z y = z
10 7 9 mpd F : A 1-1 B y A z A y = z
11 10 3expia F : A 1-1 B y A z A y = z
12 11 ralrimiv F : A 1-1 B y A z A y = z
13 12 reximdva0 F : A 1-1 B A y A z A y = z
14 issn y A z A y = z x A = x
15 13 14 syl F : A 1-1 B A x A = x