Theorem 0fv 6922

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 4291	. . 3 ⊢ ¬ 𝐴 ∈ ∅
2		dm0 5910	. . . 4 ⊢ dom ∅ = ∅
3	2	eleq2i 2855	. . 3 ⊢ (𝐴 ∈ dom ∅ ↔ 𝐴 ∈ ∅)
4	1, 3	mtbir 326	. 2 ⊢ ¬ 𝐴 ∈ dom ∅
5		ndmfv 6913	. 2 ⊢ (¬ 𝐴 ∈ dom ∅ → (∅‘𝐴) = ∅)
6	4, 5	ax-mp 5	1 ⊢ (∅‘𝐴) = ∅

Syntax hints:  ¬ wn 3   = wceq 1570   ∈ wcel 2143  ∅c0 4286  dom cdm 5661  ‘cfv 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-nul 5269  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-dm 5671  df-iota 6492  df-fv 6544

This theorem is referenced by:  fv2prc  6923  csbfv12  6926  0ov  7447  elfvov1  7452  elfvov2  7453  csbov123  7454  csbov  7455  elovmpt3imp  7667  bropopvvv  8081  bropfvvvvlem  8082  itunisuc  10398  ccat1st1st  14662  str0  17244  cntrval  19384  cntzval  19386  cntzrcl  19392  rlmval  21312  chrval  21673  ocvval  21817  elocv  21818  opsrle  22198  opsrbaslem  22200  mpfrcl  22236  evlval  22251  psr1val  22346  vr1val  22352  iscnp2  23396  resvsca  33652  constrext2chnlem  34140  mrsubfval  36000  msubfval  36016  poimirlem28  38319  0cnv  46476  elfvne0  49647  prcof1  50186