Theorem 0fv 6935

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

Syntax hints:  ¬ wn 3   = wceq 1540   ∈ wcel 2105  ∅c0 4322  dom cdm 5676  ‘cfv 6543

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-dm 5686  df-iota 6495  df-fv 6551

This theorem is referenced by:  fv2prc  6936  csbfv12  6939  0ov  7449  csbov123  7454  csbov  7455  elovmpt3imp  7667  bropopvvv  8081  bropfvvvvlem  8082  itunisuc  10420  ccat1st1st  14585  str0  17129  ressbasOLD  17187  cntrval  19231  cntzval  19233  cntzrcl  19239  rlmval  21043  chrval  21388  ocvval  21531  elocv  21532  opsrle  21914  opsrbaslem  21916  opsrbaslemOLD  21917  mpfrcl  21960  evlval  21970  psr1val  22030  vr1val  22036  iscnp2  23064  resvsca  32882  mrsubfval  34965  msubfval  34981  poimirlem28  36983  0cnv  44920  elfvne0  47680