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

Theorem ndmfv 5405
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
StepHypRef Expression
1 euex 2136 . . . . 5  |-  ( E! y  A F y  ->  E. y  A F y )
2 eldmg 4781 . . . . 5  |-  ( A  e.  _V  ->  ( A  e.  dom  F  <->  E. y  A F y ) )
31, 2syl5ibr 214 . . . 4  |-  ( A  e.  _V  ->  ( E! y  A F
y  ->  A  e.  dom  F ) )
43con3d 127 . . 3  |-  ( A  e.  _V  ->  ( -.  A  e.  dom  F  ->  -.  E! y  A F y ) )
5 tz6.12-2 5399 . . 3  |-  ( -.  E! y  A F y  ->  ( F `  A )  =  (/) )
64, 5syl6com 33 . 2  |-  ( -.  A  e.  dom  F  ->  ( A  e.  _V  ->  ( F `  A
)  =  (/) ) )
7 fvprc 5374 . 2  |-  ( -.  A  e.  _V  ->  ( F `  A )  =  (/) )
86, 7pm2.61d1 153 1  |-  ( -.  A  e.  dom  F  ->  ( F `  A
)  =  (/) )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6   E.wex 1537    = wceq 1619    e. wcel 1621   E!weu 2114   _Vcvv 2727   (/)c0 3362   class class class wbr 3920   dom cdm 4580   ` cfv 4592
This theorem is referenced by:  ndmfvrcl  5406  elfvdm  5407  nfvres  5409  fv01  5411  funfv  5438  fvun1  5442  fvco4i  5449  fvmpti  5453  fvmptss  5461  fvmptex  5462  fvmptnf  5469  fvmptss2  5471  fvopab4ndm  5472  f0cli  5523  funiunfv  5626  ovprc  5737  oprssdm  5854  ndmovg  5855  1st2val  5997  2nd2val  5998  curry1val  6063  curry2val  6067  smofvon2  6259  rdgsucmptnf  6328  frsucmptn  6337  brwitnlem  6392  undifixp  6738  r1tr  7332  rankvaln  7355  cardidm  7476  carden2a  7483  carden2b  7484  carddomi2  7487  sdomsdomcardi  7488  pm54.43lem  7516  alephcard  7581  alephnbtwn  7582  alephgeom  7593  cfub  7759  cardcf  7762  cflecard  7763  cfle  7764  cflim2  7773  cfidm  7785  itunisuc  7929  itunitc1  7930  ituniiun  7932  alephadd  8079  alephreg  8084  pwcfsdom  8085  cfpwsdom  8086  adderpq  8460  mulerpq  8461  uzssz  10126  ltweuz  10902  swrd00  11328  sumz  12072  sumss  12074  sumnul  12100  divsfval  13323  cidpropd  13457  homarcl  13704  arwval  13719  coafval  13740  iscnp2  16801  setsmstopn  17856  tngtopn  17998  pcofval  18340  dvbsss  19084  perfdvf  19085  mpfrcl  19234  dchrrcl  20311  vsfval  21021  dmadjrnb  22316  hmdmadj  22350  rdgprc0  23318  soseq  23422  nofv  23478  sltres  23485  bdayelon  23501  axdenselem2  23504  fullfunfv  23659  eleenn  23698  linedegen  23940  fvsnn  24279  itgocn  26535  matrcl  26632  dibvalrel  30042  dicvalrelN  30064  dihvalrel  30158
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-sep 4038  ax-nul 4046  ax-pr 4108
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-eu 2118  df-mo 2119  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-ral 2513  df-rex 2514  df-rab 2516  df-v 2729  df-sbc 2922  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-nul 3363  df-if 3471  df-sn 3550  df-pr 3551  df-op 3553  df-uni 3728  df-br 3921  df-opab 3975  df-xp 4594  df-cnv 4596  df-dm 4598  df-rn 4599  df-res 4600  df-ima 4601  df-fv 4608
  Copyright terms: Public domain W3C validator