Theorem fvfundmfvn0 6876

Description: If the "value of a class" at an argument is not the empty set, then the argument is in the domain of the class and the class restricted to the singleton formed on that argument is a function. (Contributed by Alexander van der Vekens, 26-May-2017.) (Proof shortened by BJ, 13-Aug-2022.)

Assertion

Ref	Expression
fvfundmfvn0	⊢ ((𝐹‘𝐴) ≠ ∅ → (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})))

Proof of Theorem fvfundmfvn0

Step	Hyp	Ref	Expression
1		ndmfv 6868	. . 3 ⊢ (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅)
2	1	necon1ai 2960	. 2 ⊢ ((𝐹‘𝐴) ≠ ∅ → 𝐴 ∈ dom 𝐹)
3		nfunsn 6875	. . 3 ⊢ (¬ Fun (𝐹 ↾ {𝐴}) → (𝐹‘𝐴) = ∅)
4	3	necon1ai 2960	. 2 ⊢ ((𝐹‘𝐴) ≠ ∅ → Fun (𝐹 ↾ {𝐴}))
5	2, 4	jca 511	1 ⊢ ((𝐹‘𝐴) ≠ ∅ → (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   ≠ wne 2933  ∅c0 4274  {csn 4568  dom cdm 5626   ↾ cres 5628  Fun wfun 6488  ‘cfv 6494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-id 5521  df-xp 5632  df-rel 5633  df-cnv 5634  df-co 5635  df-dm 5636  df-res 5638  df-iota 6450  df-fun 6496  df-fv 6502

This theorem is referenced by:  fvn0ssdmfun  7022  feldmfvelcdm  7034  umgrnloopv  29193  usgrnloopvALT  29288  afvpcfv0  47610  afvfvn0fveq  47614  afv0nbfvbi  47615  afv2fvn0fveq  47728  ovn0dmfun  48648  reldmlan2  50108  reldmran2  50109  lanrcl  50112  ranrcl  50113  lmdran  50162  cmdlan  50163