Theorem 0fv 6265

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 3952	. . 3 ⊢ ¬ 𝐴 ∈ ∅
2		dm0 5371	. . . 4 ⊢ dom ∅ = ∅
3	2	eleq2i 2722	. . 3 ⊢ (𝐴 ∈ dom ∅ ↔ 𝐴 ∈ ∅)
4	1, 3	mtbir 312	. 2 ⊢ ¬ 𝐴 ∈ dom ∅
5		ndmfv 6256	. 2 ⊢ (¬ 𝐴 ∈ dom ∅ → (∅‘𝐴) = ∅)
6	4, 5	ax-mp 5	1 ⊢ (∅‘𝐴) = ∅

Syntax hints:  ¬ wn 3   = wceq 1523   ∈ wcel 2030  ∅c0 3948  dom cdm 5143  ‘cfv 5926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-nul 4822  ax-pow 4873

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-dm 5153  df-iota 5889  df-fv 5934

This theorem is referenced by:  fv2prc  6266  csbfv12  6269  0ov  6722  csbov123  6727  csbov  6728  elovmpt3imp  6932  bropopvvv  7300  bropfvvvvlem  7301  itunisuc  9279  itunitc1  9280  ccat1st1st  13448  str0  15958  ressbas  15977  cntrval  17798  cntzval  17800  cntzrcl  17806  sralem  19225  srasca  19229  sravsca  19230  sraip  19231  rlmval  19239  opsrle  19523  opsrbaslem  19525  opsrbaslemOLD  19526  mpfrcl  19566  evlval  19572  psr1val  19604  vr1val  19610  chrval  19921  ocvval  20059  elocv  20060  iscnp2  21091  resvsca  29958  mrsubfval  31531  msubfval  31547  poimirlem28  33567  0cnv  40292