MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  0fv Structured version   Visualization version   GIF version

Theorem 0fv 6702
Description: Function value of the empty set. (Contributed by Stefan O'Rear, 26-Nov-2014.)
Assertion
Ref Expression
0fv (∅‘𝐴) = ∅

Proof of Theorem 0fv
StepHypRef Expression
1 noel 4293 . . 3 ¬ 𝐴 ∈ ∅
2 dm0 5783 . . . 4 dom ∅ = ∅
32eleq2i 2901 . . 3 (𝐴 ∈ dom ∅ ↔ 𝐴 ∈ ∅)
41, 3mtbir 324 . 2 ¬ 𝐴 ∈ dom ∅
5 ndmfv 6693 . 2 𝐴 ∈ dom ∅ → (∅‘𝐴) = ∅)
64, 5ax-mp 5 1 (∅‘𝐴) = ∅
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1528  wcel 2105  c0 4288  dom cdm 5548  cfv 6348
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-nul 5201  ax-pow 5257
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-dm 5558  df-iota 6307  df-fv 6356
This theorem is referenced by:  fv2prc  6703  csbfv12  6706  0ov  7182  csbov123  7187  csbov  7188  elovmpt3imp  7391  bropopvvv  7774  bropfvvvvlem  7775  itunisuc  9829  ccat1st1st  13972  str0  16523  ressbas  16542  cntrval  18387  cntzval  18389  cntzrcl  18395  rlmval  19892  opsrle  20184  opsrbaslem  20186  mpfrcl  20226  evlval  20236  psr1val  20282  vr1val  20288  chrval  20600  ocvval  20739  elocv  20740  iscnp2  21775  resvsca  30830  mrsubfval  32652  msubfval  32668  poimirlem28  34801  0cnv  41899
  Copyright terms: Public domain W3C validator