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

Theorem ndmfv 5568
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 2179 . . . . 5  |-  ( E! x  A F x  ->  E. x  A F x )
2 eldmg 4890 . . . . 5  |-  ( A  e.  _V  ->  ( A  e.  dom  F  <->  E. x  A F x ) )
31, 2syl5ibr 212 . . . 4  |-  ( A  e.  _V  ->  ( E! x  A F x  ->  A  e.  dom  F ) )
43con3d 125 . . 3  |-  ( A  e.  _V  ->  ( -.  A  e.  dom  F  ->  -.  E! x  A F x ) )
5 tz6.12-2 5532 . . 3  |-  ( -.  E! x  A F x  ->  ( F `  A )  =  (/) )
64, 5syl6 29 . 2  |-  ( A  e.  _V  ->  ( -.  A  e.  dom  F  ->  ( F `  A )  =  (/) ) )
7 fvprc 5535 . . 3  |-  ( -.  A  e.  _V  ->  ( F `  A )  =  (/) )
87a1d 22 . 2  |-  ( -.  A  e.  _V  ->  ( -.  A  e.  dom  F  ->  ( F `  A )  =  (/) ) )
96, 8pm2.61i 156 1  |-  ( -.  A  e.  dom  F  ->  ( F `  A
)  =  (/) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   E.wex 1531    = wceq 1632    e. wcel 1696   E!weu 2156   _Vcvv 2801   (/)c0 3468   class class class wbr 4039   dom cdm 4705   ` cfv 5271
This theorem is referenced by:  ndmfvrcl  5569  elfvdm  5570  nfvres  5573  fv01  5575  funfv  5602  fvun1  5606  fvco4i  5613  fvmpti  5617  fvmptss  5625  fvmptex  5626  fvmptnf  5633  fvmptss2  5635  fvopab4ndm  5636  f0cli  5687  funiunfv  5790  ovprc  5901  oprssdm  6018  ndmovg  6019  1st2val  6161  2nd2val  6162  curry1val  6227  curry2val  6231  smofvon2  6389  rdgsucmptnf  6458  frsucmptn  6467  brwitnlem  6522  undifixp  6868  r1tr  7464  rankvaln  7487  cardidm  7608  carden2a  7615  carden2b  7616  carddomi2  7619  sdomsdomcardi  7620  pm54.43lem  7648  alephcard  7713  alephnbtwn  7714  alephgeom  7725  cfub  7891  cardcf  7894  cflecard  7895  cfle  7896  cflim2  7905  cfidm  7917  itunisuc  8061  itunitc1  8062  ituniiun  8064  alephadd  8215  alephreg  8220  pwcfsdom  8221  cfpwsdom  8222  adderpq  8596  mulerpq  8597  uzssz  10263  ltweuz  11040  swrd00  11467  sumz  12211  sumss  12213  sumnul  12239  divsfval  13465  cidpropd  13629  homarcl  13876  arwval  13891  coafval  13912  iscnp2  16985  setsmstopn  18040  tngtopn  18182  pcofval  18524  dvbsss  19268  perfdvf  19269  mpfrcl  19418  dchrrcl  20495  vsfval  21207  dmadjrnb  22502  hmdmadj  22536  gsumpropd2lem  23394  prod1  24169  rdgprc0  24221  soseq  24325  nofv  24382  sltres  24389  bdayelon  24405  fvnobday  24407  fullfunfv  24557  eleenn  24596  linedegen  24838  fvsnn  25217  itgocn  27472  matrcl  27569  fvfundmfvn0  28091  nssdmovg  28194  trlonprop  28341  dibvalrel  31975  dicvalrelN  31997  dihvalrel  32091
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-nul 4165  ax-pow 4204
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-dm 4715  df-iota 5235  df-fv 5279
  Copyright terms: Public domain W3C validator