Theorem fvfundmfvn0 6921

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 6913	. . 3 ⊢ (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅)
2	1	necon1ai 2984	. 2 ⊢ ((𝐹‘𝐴) ≠ ∅ → 𝐴 ∈ dom 𝐹)
3		nfunsn 6920	. . 3 ⊢ (¬ Fun (𝐹 ↾ {𝐴}) → (𝐹‘𝐴) = ∅)
4	3	necon1ai 2984	. 2 ⊢ ((𝐹‘𝐴) ≠ ∅ → Fun (𝐹 ↾ {𝐴}))
5	2, 4	jca 520	1 ⊢ ((𝐹‘𝐴) ≠ ∅ → (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})))

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∈ wcel 2142   ≠ wne 2957  ∅c0 4285  {csn 4588  dom cdm 5660   ↾ cres 5662  Fun wfun 6530  ‘cfv 6536

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5256  ax-nul 5268  ax-pr 5403

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-opab 5173  df-id 5555  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-res 5672  df-iota 6492  df-fun 6538  df-fv 6544

This theorem is used by:  fvn0ssdmfun  7069  feldmfvelcdm  7081  umgrnloopv  29467  usgrnloopvALT  29562  kardcard2a  35585  afvpcfv0  47911  afvfvn0fveq  47915  afv0nbfvbi  47916  afv2fvn0fveq  48029  ovn0dmfun  48949  reldmlan2  50423  reldmran2  50424  lanrcl  50427  ranrcl  50428  lmdran  50477  cmdlan  50478