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

Theorem ndmfv 5513
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  y is distinct from all other variables.
StepHypRef Expression
1 euex 2166 . . . . 5  |-  ( E! y  A F y  ->  E. y  A F y )
2 eldmg 4872 . . . . 5  |-  ( A  e.  _V  ->  ( A  e.  dom  F  <->  E. y  A F y ) )
31, 2syl5ibr 212 . . . 4  |-  ( A  e.  _V  ->  ( E! y  A F
y  ->  A  e.  dom  F ) )
43con3d 125 . . 3  |-  ( A  e.  _V  ->  ( -.  A  e.  dom  F  ->  -.  E! y  A F y ) )
5 tz6.12-2 5507 . . 3  |-  ( -.  E! y  A F y  ->  ( F `  A )  =  (/) )
64, 5syl6com 31 . 2  |-  ( -.  A  e.  dom  F  ->  ( A  e.  _V  ->  ( F `  A
)  =  (/) ) )
7 fvprc 5482 . 2  |-  ( -.  A  e.  _V  ->  ( F `  A )  =  (/) )
86, 7pm2.61d1 151 1  |-  ( -.  A  e.  dom  F  ->  ( F `  A
)  =  (/) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   E.wex 1528    = wceq 1623    e. wcel 1684   E!weu 2143   _Vcvv 2788   (/)c0 3455   class class class wbr 4023   dom cdm 4687   ` cfv 5220
This theorem is referenced by:  ndmfvrcl  5514  elfvdm  5515  nfvres  5518  fv01  5520  funfv  5547  fvun1  5551  fvco4i  5558  fvmpti  5562  fvmptss  5570  fvmptex  5571  fvmptnf  5578  fvmptss2  5580  fvopab4ndm  5581  f0cli  5632  funiunfv  5735  ovprc  5846  oprssdm  5963  ndmovg  5964  1st2val  6106  2nd2val  6107  curry1val  6172  curry2val  6176  smofvon2  6368  rdgsucmptnf  6437  frsucmptn  6446  brwitnlem  6501  undifixp  6847  r1tr  7443  rankvaln  7466  cardidm  7587  carden2a  7594  carden2b  7595  carddomi2  7598  sdomsdomcardi  7599  pm54.43lem  7627  alephcard  7692  alephnbtwn  7693  alephgeom  7704  cfub  7870  cardcf  7873  cflecard  7874  cfle  7875  cflim2  7884  cfidm  7896  itunisuc  8040  itunitc1  8041  ituniiun  8043  alephadd  8194  alephreg  8199  pwcfsdom  8200  cfpwsdom  8201  adderpq  8575  mulerpq  8576  uzssz  10242  ltweuz  11019  swrd00  11446  sumz  12190  sumss  12192  sumnul  12218  divsfval  13444  cidpropd  13608  homarcl  13855  arwval  13870  coafval  13891  iscnp2  16964  setsmstopn  18019  tngtopn  18161  pcofval  18503  dvbsss  19247  perfdvf  19248  mpfrcl  19397  dchrrcl  20474  vsfval  21184  dmadjrnb  22481  hmdmadj  22515  rdgprc0  23553  soseq  23657  nofv  23713  sltres  23720  bdayelon  23736  axdenselem2  23739  fullfunfv  23894  eleenn  23933  linedegen  24175  fvsnn  24524  itgocn  26780  matrcl  26877  fvfundmfvn0  27397  dibvalrel  30656  dicvalrelN  30678  dihvalrel  30772
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4186  ax-pr 4212
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-xp 4693  df-cnv 4695  df-dm 4697  df-rn 4698  df-res 4699  df-ima 4700  df-fv 5228
  Copyright terms: Public domain W3C validator