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

Theorem ndmfv 5486
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 2141 . . . . 5  |-  ( E! y  A F y  ->  E. y  A F y )
2 eldmg 4862 . . . . 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 5480 . . 3  |-  ( -.  E! y  A F y  ->  ( F `  A )  =  (/) )
64, 5syl6com 33 . 2  |-  ( -.  A  e.  dom  F  ->  ( A  e.  _V  ->  ( F `  A
)  =  (/) ) )
7 fvprc 5455 . 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 2118   _Vcvv 2763   (/)c0 3430   class class class wbr 3997   dom cdm 4661   ` cfv 4673
This theorem is referenced by:  ndmfvrcl  5487  elfvdm  5488  nfvres  5491  fv01  5493  funfv  5520  fvun1  5524  fvco4i  5531  fvmpti  5535  fvmptss  5543  fvmptex  5544  fvmptnf  5551  fvmptss2  5553  fvopab4ndm  5554  f0cli  5605  funiunfv  5708  ovprc  5819  oprssdm  5936  ndmovg  5937  1st2val  6079  2nd2val  6080  curry1val  6145  curry2val  6149  smofvon2  6341  rdgsucmptnf  6410  frsucmptn  6419  brwitnlem  6474  undifixp  6820  r1tr  7416  rankvaln  7439  cardidm  7560  carden2a  7567  carden2b  7568  carddomi2  7571  sdomsdomcardi  7572  pm54.43lem  7600  alephcard  7665  alephnbtwn  7666  alephgeom  7677  cfub  7843  cardcf  7846  cflecard  7847  cfle  7848  cflim2  7857  cfidm  7869  itunisuc  8013  itunitc1  8014  ituniiun  8016  alephadd  8167  alephreg  8172  pwcfsdom  8173  cfpwsdom  8174  adderpq  8548  mulerpq  8549  uzssz  10215  ltweuz  10991  swrd00  11417  sumz  12161  sumss  12163  sumnul  12189  divsfval  13412  cidpropd  13576  homarcl  13823  arwval  13838  coafval  13859  iscnp2  16932  setsmstopn  17987  tngtopn  18129  pcofval  18471  dvbsss  19215  perfdvf  19216  mpfrcl  19365  dchrrcl  20442  vsfval  21152  dmadjrnb  22447  hmdmadj  22481  rdgprc0  23520  soseq  23624  nofv  23680  sltres  23687  bdayelon  23703  axdenselem2  23706  fullfunfv  23861  eleenn  23900  linedegen  24142  fvsnn  24481  itgocn  26737  matrcl  26834  dibvalrel  30603  dicvalrelN  30625  dihvalrel  30719
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 2239  ax-sep 4115  ax-nul 4123  ax-pr 4186
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 2122  df-mo 2123  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-ral 2523  df-rex 2524  df-rab 2527  df-v 2765  df-sbc 2967  df-dif 3130  df-un 3132  df-in 3134  df-ss 3141  df-nul 3431  df-if 3540  df-sn 3620  df-pr 3621  df-op 3623  df-uni 3802  df-br 3998  df-opab 4052  df-xp 4675  df-cnv 4677  df-dm 4679  df-rn 4680  df-res 4681  df-ima 4682  df-fv 4689
  Copyright terms: Public domain W3C validator