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

Theorem ndmfv 5451
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 2139 . . . . 5  |-  ( E! y  A F y  ->  E. y  A F y )
2 eldmg 4827 . . . . 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 5445 . . 3  |-  ( -.  E! y  A F y  ->  ( F `  A )  =  (/) )
64, 5syl6com 33 . 2  |-  ( -.  A  e.  dom  F  ->  ( A  e.  _V  ->  ( F `  A
)  =  (/) ) )
7 fvprc 5420 . 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 2117   _Vcvv 2740   (/)c0 3397   class class class wbr 3963   dom cdm 4626   ` cfv 4638
This theorem is referenced by:  ndmfvrcl  5452  elfvdm  5453  nfvres  5456  fv01  5458  funfv  5485  fvun1  5489  fvco4i  5496  fvmpti  5500  fvmptss  5508  fvmptex  5509  fvmptnf  5516  fvmptss2  5518  fvopab4ndm  5519  f0cli  5570  funiunfv  5673  ovprc  5784  oprssdm  5901  ndmovg  5902  1st2val  6044  2nd2val  6045  curry1val  6110  curry2val  6114  smofvon2  6306  rdgsucmptnf  6375  frsucmptn  6384  brwitnlem  6439  undifixp  6785  r1tr  7381  rankvaln  7404  cardidm  7525  carden2a  7532  carden2b  7533  carddomi2  7536  sdomsdomcardi  7537  pm54.43lem  7565  alephcard  7630  alephnbtwn  7631  alephgeom  7642  cfub  7808  cardcf  7811  cflecard  7812  cfle  7813  cflim2  7822  cfidm  7834  itunisuc  7978  itunitc1  7979  ituniiun  7981  alephadd  8132  alephreg  8137  pwcfsdom  8138  cfpwsdom  8139  adderpq  8513  mulerpq  8514  uzssz  10179  ltweuz  10955  swrd00  11381  sumz  12125  sumss  12127  sumnul  12153  divsfval  13376  cidpropd  13540  homarcl  13787  arwval  13802  coafval  13823  iscnp2  16896  setsmstopn  17951  tngtopn  18093  pcofval  18435  dvbsss  19179  perfdvf  19180  mpfrcl  19329  dchrrcl  20406  vsfval  21116  dmadjrnb  22411  hmdmadj  22445  rdgprc0  23484  soseq  23588  nofv  23644  sltres  23651  bdayelon  23667  axdenselem2  23670  fullfunfv  23825  eleenn  23864  linedegen  24106  fvsnn  24445  itgocn  26701  matrcl  26798  dibvalrel  30483  dicvalrelN  30505  dihvalrel  30599
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 1927  ax-ext 2237  ax-sep 4081  ax-nul 4089  ax-pr 4152
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 1884  df-eu 2121  df-mo 2122  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-ral 2520  df-rex 2521  df-rab 2523  df-v 2742  df-sbc 2936  df-dif 3097  df-un 3099  df-in 3101  df-ss 3108  df-nul 3398  df-if 3507  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3769  df-br 3964  df-opab 4018  df-xp 4640  df-cnv 4642  df-dm 4644  df-rn 4645  df-res 4646  df-ima 4647  df-fv 4654
  Copyright terms: Public domain W3C validator