Theorem nfunsn 4831

Description: If the restriction of a class to a singleton is not a function, its value is the empty set. (The proof was shortened by Andrew Salmon, 22-Oct-2011.)

Assertion

Ref	Expression
nfunsn	|- (-. Fun (F |` {A}) -> (F` A) = (/))

Proof of Theorem nfunsn

Step	Hyp	Ref	Expression
1		eumo 2101	. . . . . . 7 |- (E!y AFy -> E*y AFy)
2		visset 2572	. . . . . . . . . 10 |- y e. _V
3	2	brres 4378	. . . . . . . . 9 |- (x(F |` {A})y <-> (xFy /\ x e. {A}))
4		elsn 3283	. . . . . . . . . . 11 |- (x e. {A} <-> x = A)
5		breq1 3542	. . . . . . . . . . 11 |- (x = A -> (xFy <-> AFy))
6	4, 5	sylbi 237	. . . . . . . . . 10 |- (x e. {A} -> (xFy <-> AFy))
7	6	biimpac 713	. . . . . . . . 9 |- ((xFy /\ x e. {A}) -> AFy)
8	3, 7	sylbi 237	. . . . . . . 8 |- (x(F |` {A})y -> AFy)
9	8	immoi 2108	. . . . . . 7 |- (E*y AFy -> E*y x(F |` {A})y)
10	1, 9	syl 13	. . . . . 6 |- (E!y AFy -> E*y x(F |` {A})y)
11		tz6.12-2 4824	. . . . . 6 |- (-. E!y AFy -> (F` A) = (/))
12	10, 11	nsyl4 179	. . . . 5 |- (-. (F` A) = (/) -> E*y x(F |` {A})y)
13	12	19.21aiv 1962	. . . 4 |- (-. (F` A) = (/) -> A.xE*y x(F |` {A})y)
14		relres 4395	. . . 4 |- Rel (F |` {A})
15	13, 14	jctil 597	. . 3 |- (-. (F` A) = (/) -> (Rel (F |` {A}) /\ A.xE*y x(F |` {A})y))
16		dffun6 4578	. . 3 |- (Fun (F |` {A}) <-> (Rel (F |` {A}) /\ A.xE*y x(F |` {A})y))
17	15, 16	sylibr 264	. 2 |- (-. (F` A) = (/) -> Fun (F |` {A}))
18	17	con1i 156	1 |- (-. Fun (F |` {A}) -> (F` A) = (/))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 231   /\ wa 433  A.wal 1613   = wceq 1615   e. wcel 1617  E!weu 2066  E*wmo 2067  (/)c0 3114  {csn 3270   class class class wbr 3539   |` cres 4153  Rel wrel 4156  Fun wfun 4157  ` cfv 4163

This theorem is referenced by:  dffv2 4859

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-9 1624  ax-10 1625  ax-11 1626  ax-12 1627  ax-14 1629  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152  ax-sep 3638  ax-nul 3645  ax-pow 3681  ax-pr 3719

This theorem depends on definitions:  df-bi 232  df-or 434  df-an 435  df-ex 1645  df-sb 1845  df-eu 2070  df-mo 2071  df-clab 2158  df-cleq 2163  df-clel 2166  df-ne 2297  df-ral 2389  df-rex 2390  df-v 2571  df-dif 2862  df-un 2864  df-in 2866  df-ss 2868  df-nul 3115  df-pw 3261  df-sn 3274  df-pr 3275  df-op 3278  df-uni 3399  df-br 3540  df-opab 3598  df-id 3779  df-xp 4165  df-rel 4166  df-cnv 4167  df-co 4168  df-dm 4169  df-rn 4170  df-res 4171  df-ima 4172  df-fun 4173  df-fv 4179

Copyright terms: Public domain