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

Theorem ndmfv 5702
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 2279 . . . . 5  |-  ( E! x  A F x  ->  E. x  A F x )
2 eldmg 5022 . . . . 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 5670 . . 3  |-  ( -.  E! x  A F x  ->  ( F `  A )  =  (/) )
64, 5syl6 33 . 2  |-  ( A  e.  _V  ->  ( -.  A  e.  dom  F  ->  ( F `  A )  =  (/) ) )
7 fvprc 5673 . . 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 1362   E.wex 1589    e. wcel 1755   E!weu 2254   _Vcvv 2962   (/)c0 3625   class class class wbr 4280   dom cdm 4827   ` cfv 5406
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-nul 4409  ax-pow 4458
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-dm 4837  df-iota 5369  df-fv 5414
This theorem is referenced by:  ndmfvrcl  5703  elfvdm  5704  nfvres  5708  fvfundmfvn0  5710  0fv  5711  funfv  5746  fvun1  5750  fvco4i  5757  fvmpti  5761  fvmptss  5770  fvmptex  5772  fvmptnf  5779  fvmptss2  5781  fvopab4ndm  5782  f0cli  5842  funiunfv  5952  ovprc  6107  oprssdm  6233  nssdmovg  6234  ndmovg  6235  1st2val  6591  2nd2val  6592  bropopvvv  6642  curry1val  6654  curry2val  6658  smofvon2  6803  rdgsucmptnf  6871  frsucmptn  6880  brwitnlem  6935  undifixp  7287  r1tr  7971  rankvaln  7994  cardidm  8117  carden2a  8124  carden2b  8125  carddomi2  8128  sdomsdomcardi  8129  pm54.43lem  8157  alephcard  8228  alephnbtwn  8229  alephgeom  8240  cfub  8406  cardcf  8409  cflecard  8410  cfle  8411  cflim2  8420  cfidm  8432  itunisuc  8576  itunitc1  8577  ituniiun  8579  alephadd  8729  alephreg  8734  pwcfsdom  8735  cfpwsdom  8736  adderpq  9112  mulerpq  9113  uzssz  10867  ltweuz  11767  wrdsymb0  12242  lsw0  12250  swrd00  12297  swrd0  12310  sumz  13182  sumss  13184  sumnul  13210  divsfval  14467  cidpropd  14631  homarcl  14878  arwval  14893  coafval  14914  lubval  15136  glbval  15149  joinval  15157  meetval  15171  iscnp2  18684  setsmstopn  19894  tngtopn  20077  pcofval  20423  dvbsss  21218  perfdvf  21219  mpfrcl  21369  dchrrcl  22463  eleenn  22964  vsfval  23835  dmadjrnb  25132  hmdmadj  25166  gsumpropd2lem  26092  prod1  27303  prodss  27306  rdgprc0  27453  soseq  27561  nofv  27644  sltres  27651  bdayelon  27667  fvnobday  27669  fullfunfv  27824  linedegen  28020  itgocn  29363  elfvmptrab1  29997  2wlkonot3v  30237  2spthonot3v  30238  clwwlknprop  30278  bj-inftyexpidisj  32110  dibvalrel  34378  dicvalrelN  34400  dihvalrel  34494
  Copyright terms: Public domain W3C validator