Theorem 0fv 6875

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 4290	. . 3 ⊢ ¬ 𝐴 ∈ ∅
2		dm0 5869	. . . 4 ⊢ dom ∅ = ∅
3	2	eleq2i 2828	. . 3 ⊢ (𝐴 ∈ dom ∅ ↔ 𝐴 ∈ ∅)
4	1, 3	mtbir 323	. 2 ⊢ ¬ 𝐴 ∈ dom ∅
5		ndmfv 6866	. 2 ⊢ (¬ 𝐴 ∈ dom ∅ → (∅‘𝐴) = ∅)
6	4, 5	ax-mp 5	1 ⊢ (∅‘𝐴) = ∅

Syntax hints:  ¬ wn 3   = wceq 1541   ∈ wcel 2113  ∅c0 4285  dom cdm 5624  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-dm 5634  df-iota 6448  df-fv 6500

This theorem is referenced by:  fv2prc  6876  csbfv12  6879  0ov  7395  elfvov1  7400  elfvov2  7401  csbov123  7402  csbov  7403  elovmpt3imp  7615  bropopvvv  8032  bropfvvvvlem  8033  itunisuc  10329  ccat1st1st  14552  str0  17116  cntrval  19248  cntzval  19250  cntzrcl  19256  rlmval  21143  chrval  21478  ocvval  21622  elocv  21623  opsrle  22002  opsrbaslem  22004  mpfrcl  22040  evlval  22055  psr1val  22126  vr1val  22132  iscnp2  23183  resvsca  33413  constrext2chnlem  33907  mrsubfval  35702  msubfval  35718  poimirlem28  37849  0cnv  45986  elfvne0  49094  prcof1  49633