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

Theorem ndmfv 5756
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 2305 . . . . 5  |-  ( E! x  A F x  ->  E. x  A F x )
2 eldmg 5066 . . . . 5  |-  ( A  e.  _V  ->  ( A  e.  dom  F  <->  E. x  A F x ) )
31, 2syl5ibr 214 . . . 4  |-  ( A  e.  _V  ->  ( E! x  A F x  ->  A  e.  dom  F ) )
43con3d 128 . . 3  |-  ( A  e.  _V  ->  ( -.  A  e.  dom  F  ->  -.  E! x  A F x ) )
5 tz6.12-2 5720 . . 3  |-  ( -.  E! x  A F x  ->  ( F `  A )  =  (/) )
64, 5syl6 32 . 2  |-  ( A  e.  _V  ->  ( -.  A  e.  dom  F  ->  ( F `  A )  =  (/) ) )
7 fvprc 5723 . . 3  |-  ( -.  A  e.  _V  ->  ( F `  A )  =  (/) )
87a1d 24 . 2  |-  ( -.  A  e.  _V  ->  ( -.  A  e.  dom  F  ->  ( F `  A )  =  (/) ) )
96, 8pm2.61i 159 1  |-  ( -.  A  e.  dom  F  ->  ( F `  A
)  =  (/) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   E.wex 1551    = wceq 1653    e. wcel 1726   E!weu 2282   _Vcvv 2957   (/)c0 3629   class class class wbr 4213   dom cdm 4879   ` cfv 5455
This theorem is referenced by:  ndmfvrcl  5757  elfvdm  5758  nfvres  5761  fvfundmfvn0  5763  fv01  5764  funfv  5791  fvun1  5795  fvco4i  5802  fvmpti  5806  fvmptss  5814  fvmptex  5816  fvmptnf  5823  fvmptss2  5825  fvopab4ndm  5826  f0cli  5881  funiunfv  5996  ovprc  6109  oprssdm  6229  nssdmovg  6230  ndmovg  6231  1st2val  6373  2nd2val  6374  bropopvvv  6427  curry1val  6440  curry2val  6444  smofvon2  6619  rdgsucmptnf  6688  frsucmptn  6697  brwitnlem  6752  undifixp  7099  r1tr  7703  rankvaln  7726  cardidm  7847  carden2a  7854  carden2b  7855  carddomi2  7858  sdomsdomcardi  7859  pm54.43lem  7887  alephcard  7952  alephnbtwn  7953  alephgeom  7964  cfub  8130  cardcf  8133  cflecard  8134  cfle  8135  cflim2  8144  cfidm  8156  itunisuc  8300  itunitc1  8301  ituniiun  8303  alephadd  8453  alephreg  8458  pwcfsdom  8459  cfpwsdom  8460  adderpq  8834  mulerpq  8835  uzssz  10506  ltweuz  11302  swrd00  11766  sumz  12517  sumss  12519  sumnul  12545  divsfval  13773  cidpropd  13937  homarcl  14184  arwval  14199  coafval  14220  iscnp2  17304  setsmstopn  18509  tngtopn  18692  pcofval  19036  dvbsss  19790  perfdvf  19791  mpfrcl  19940  dchrrcl  21025  vsfval  22115  dmadjrnb  23410  hmdmadj  23444  gsumpropd2lem  24221  prod1  25271  prodss  25274  rdgprc0  25422  soseq  25530  nofv  25613  sltres  25620  bdayelon  25636  fvnobday  25638  fullfunfv  25793  eleenn  25836  linedegen  26078  itgocn  27347  wrdsymb0  28171  lswrd0  28262  2wlkonot3v  28343  2spthonot3v  28344  dibvalrel  31962  dicvalrelN  31984  dihvalrel  32078
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418  ax-nul 4339  ax-pow 4378
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2286  df-mo 2287  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-ral 2711  df-rex 2712  df-rab 2715  df-v 2959  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-nul 3630  df-if 3741  df-sn 3821  df-pr 3822  df-op 3824  df-uni 4017  df-br 4214  df-dm 4889  df-iota 5419  df-fv 5463
  Copyright terms: Public domain W3C validator