Prove f1cdmsn

set.mm

@@ -68516,6 +68516,19 @@ more bytes (305 versus 282).  (Contributed by AV, 3-Feb-2021.)
       UOUPURWFVBCVIHZWHWFWIVBWFWIEBCULUMUNUOUQ $.
   $}
 
+  ${
+    $d A x y $.  $d A y z $.  $d B y z $.  $d F y z $.
+    $( 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.) $)
+    f1cdmsn $p |- ( ( F : A -1-1-> { B } /\ A =/= (/) ) -> E. x A = { x } ) $=
+      ( vy vz csn wf1 c0 wne wa cv wceq wral wrex wex wcel w3a cfv fvconst issn
+      wf f1f 3adant3 3adant2 eqtr4d syl3an1 f1veqaeq 3impb mpd 3expia reximdva0
+      wi ralrimiv syl ) BCGZDHZBIJKELZFLZMZFBNZEBOBALGMAPUQVAEBUQURBQZKUTFBUQVB
+      USBQZUTUQVBVCRURDSZUSDSZMZUTUQBUPDUBZVBVCVFBUPDUCVGVBVCRVDCVEVGVBVDCMVCBC
+      URDTUDVGVCVECMVBBCUSDTUEUFUGUQVBVCVFUTUMBUPURUSDUHUIUJUKUNULEFABUAUO $.
+  $}
+
   ${
     $d A f x $.  $d D f x $.  $d V f x $.  $d f ps $.  $d ph x $.
     $( TODO: there must be a more elegant way to prove this theorem using