Theorem 0fv 6905

Description: Function value of the empty set. (Contributed by Stefan O'Rear, 26-Nov-2014.)

Assertion

Ref	Expression
0fv	⊢ (∅‘𝐴) = ∅

Proof of Theorem 0fv

Step	Hyp	Ref	Expression
1		noel 4304	. . 3 ⊢ ¬ 𝐴 ∈ ∅
2		dm0 5887	. . . 4 ⊢ dom ∅ = ∅
3	2	eleq2i 2821	. . 3 ⊢ (𝐴 ∈ dom ∅ ↔ 𝐴 ∈ ∅)
4	1, 3	mtbir 323	. 2 ⊢ ¬ 𝐴 ∈ dom ∅
5		ndmfv 6896	. 2 ⊢ (¬ 𝐴 ∈ dom ∅ → (∅‘𝐴) = ∅)
6	4, 5	ax-mp 5	1 ⊢ (∅‘𝐴) = ∅

Syntax hints:  ¬ wn 3   = wceq 1540   ∈ wcel 2109  ∅c0 4299  dom cdm 5641  ‘cfv 6514

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-dm 5651  df-iota 6467  df-fv 6522

This theorem is referenced by:  fv2prc  6906  csbfv12  6909  0ov  7427  elfvov1  7432  elfvov2  7433  csbov123  7434  csbov  7435  elovmpt3imp  7649  bropopvvv  8072  bropfvvvvlem  8073  itunisuc  10379  ccat1st1st  14600  str0  17166  cntrval  19258  cntzval  19260  cntzrcl  19266  rlmval  21105  chrval  21440  ocvval  21583  elocv  21584  opsrle  21961  opsrbaslem  21963  mpfrcl  21999  evlval  22009  psr1val  22077  vr1val  22083  iscnp2  23133  resvsca  33311  constrext2chnlem  33747  mrsubfval  35502  msubfval  35518  poimirlem28  37649  0cnv  45747  elfvne0  48841  prcof1  49381