MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ndmfv Structured version   Unicode version

Theorem ndmfv 5876
Description: The value of a class outside its domain is the empty set. (Contributed by NM, 24-Aug-1995.)
Assertion
Ref Expression
ndmfv  |-  ( -.  A  e.  dom  F  ->  ( F `  A
)  =  (/) )

Proof of Theorem ndmfv
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 euex 2292 . . . . 5  |-  ( E! x  A F x  ->  E. x  A F x )
2 eldmg 5184 . . . . 5  |-  ( A  e.  _V  ->  ( A  e.  dom  F  <->  E. x  A F x ) )
31, 2syl5ibr 221 . . . 4  |-  ( A  e.  _V  ->  ( E! x  A F x  ->  A  e.  dom  F ) )
43con3d 133 . . 3  |-  ( A  e.  _V  ->  ( -.  A  e.  dom  F  ->  -.  E! x  A F x ) )
5 tz6.12-2 5843 . . 3  |-  ( -.  E! x  A F x  ->  ( F `  A )  =  (/) )
64, 5syl6 33 . 2  |-  ( A  e.  _V  ->  ( -.  A  e.  dom  F  ->  ( F `  A )  =  (/) ) )
7 fvprc 5846 . . 3  |-  ( -.  A  e.  _V  ->  ( F `  A )  =  (/) )
87a1d 25 . 2  |-  ( -.  A  e.  _V  ->  ( -.  A  e.  dom  F  ->  ( F `  A )  =  (/) ) )
96, 8pm2.61i 164 1  |-  ( -.  A  e.  dom  F  ->  ( F `  A
)  =  (/) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1381   E.wex 1597    e. wcel 1802   E!weu 2266   _Vcvv 3093   (/)c0 3767   class class class wbr 4433   dom cdm 4985   ` cfv 5574
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-nul 4562  ax-pow 4611
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-op 4017  df-uni 4231  df-br 4434  df-dm 4995  df-iota 5537  df-fv 5582
This theorem is referenced by:  ndmfvrcl  5877  elfvdm  5878  nfvres  5882  fvfundmfvn0  5884  0fv  5885  funfv  5921  fvun1  5925  fvco4i  5932  fvmpti  5936  fvmptss  5945  fvmptex  5947  fvmptnf  5954  fvmptss2  5956  elfvmptrab1  5957  fvopab4ndm  5959  f0cli  6023  funiunfv  6141  ovprc  6307  oprssdm  6437  nssdmovg  6438  ndmovg  6439  1st2val  6807  2nd2val  6808  bropopvvv  6861  curry1val  6874  curry2val  6878  smofvon2  7025  rdgsucmptnf  7093  frsucmptn  7102  brwitnlem  7155  undifixp  7503  r1tr  8192  rankvaln  8215  cardidm  8338  carden2a  8345  carden2b  8346  carddomi2  8349  sdomsdomcardi  8350  pm54.43lem  8378  alephcard  8449  alephnbtwn  8450  alephgeom  8461  cfub  8627  cardcf  8630  cflecard  8631  cfle  8632  cflim2  8641  cfidm  8653  itunisuc  8797  itunitc1  8798  ituniiun  8800  alephadd  8950  alephreg  8955  pwcfsdom  8956  cfpwsdom  8957  adderpq  9332  mulerpq  9333  uzssz  11104  ltweuz  12046  wrdsymb0  12549  lsw0  12560  swrd00  12619  swrd0  12632  sumz  13518  sumss  13520  sumnul  13549  divsfval  14816  cidpropd  14977  homarcl  15224  arwval  15239  coafval  15260  lubval  15483  glbval  15496  joinval  15504  meetval  15518  gsumpropd2lem  15769  mpfrcl  18055  iscnp2  19606  setsmstopn  20847  tngtopn  21030  pcofval  21376  dvbsss  22172  perfdvf  22173  dchrrcl  23380  eleenn  24064  clwwlknprop  24637  2wlkonot3v  24740  2spthonot3v  24741  vsfval  25393  dmadjrnb  26690  hmdmadj  26724  prod1  29044  prodss  29047  rdgprc0  29194  soseq  29302  nofv  29385  sltres  29392  bdayelon  29408  fvnobday  29410  fullfunfv  29565  linedegen  29761  itgocn  31082  bj-inftyexpidisj  34315  dibvalrel  36592  dicvalrelN  36614  dihvalrel  36708
  Copyright terms: Public domain W3C validator