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

Theorem ndmfv 5552
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 2166 . . . . 5  |-  ( E! x  A F x  ->  E. x  A F x )
2 eldmg 4874 . . . . 5  |-  ( A  e.  _V  ->  ( A  e.  dom  F  <->  E. x  A F x ) )
31, 2syl5ibr 212 . . . 4  |-  ( A  e.  _V  ->  ( E! x  A F x  ->  A  e.  dom  F ) )
43con3d 125 . . 3  |-  ( A  e.  _V  ->  ( -.  A  e.  dom  F  ->  -.  E! x  A F x ) )
5 tz6.12-2 5516 . . 3  |-  ( -.  E! x  A F x  ->  ( F `  A )  =  (/) )
64, 5syl6 29 . 2  |-  ( A  e.  _V  ->  ( -.  A  e.  dom  F  ->  ( F `  A )  =  (/) ) )
7 fvprc 5519 . . 3  |-  ( -.  A  e.  _V  ->  ( F `  A )  =  (/) )
87a1d 22 . 2  |-  ( -.  A  e.  _V  ->  ( -.  A  e.  dom  F  ->  ( F `  A )  =  (/) ) )
96, 8pm2.61i 156 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 4689   ` cfv 5255
This theorem is referenced by:  ndmfvrcl  5553  elfvdm  5554  nfvres  5557  fv01  5559  funfv  5586  fvun1  5590  fvco4i  5597  fvmpti  5601  fvmptss  5609  fvmptex  5610  fvmptnf  5617  fvmptss2  5619  fvopab4ndm  5620  f0cli  5671  funiunfv  5774  ovprc  5885  oprssdm  6002  ndmovg  6003  1st2val  6145  2nd2val  6146  curry1val  6211  curry2val  6215  smofvon2  6373  rdgsucmptnf  6442  frsucmptn  6451  brwitnlem  6506  undifixp  6852  r1tr  7448  rankvaln  7471  cardidm  7592  carden2a  7599  carden2b  7600  carddomi2  7603  sdomsdomcardi  7604  pm54.43lem  7632  alephcard  7697  alephnbtwn  7698  alephgeom  7709  cfub  7875  cardcf  7878  cflecard  7879  cfle  7880  cflim2  7889  cfidm  7901  itunisuc  8045  itunitc1  8046  ituniiun  8048  alephadd  8199  alephreg  8204  pwcfsdom  8205  cfpwsdom  8206  adderpq  8580  mulerpq  8581  uzssz  10247  ltweuz  11024  swrd00  11451  sumz  12195  sumss  12197  sumnul  12223  divsfval  13449  cidpropd  13613  homarcl  13860  arwval  13875  coafval  13896  iscnp2  16969  setsmstopn  18024  tngtopn  18166  pcofval  18508  dvbsss  19252  perfdvf  19253  mpfrcl  19402  dchrrcl  20479  vsfval  21191  dmadjrnb  22486  hmdmadj  22520  gsumpropd2lem  23379  rdgprc0  24150  soseq  24254  nofv  24311  sltres  24318  bdayelon  24334  fvnobday  24336  fullfunfv  24485  eleenn  24524  linedegen  24766  fvsnn  25114  itgocn  27369  matrcl  27466  fvfundmfvn0  27986  nssdmovg  28077  dibvalrel  31353  dicvalrelN  31375  dihvalrel  31469
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-nul 4149  ax-pow 4188
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-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-dm 4699  df-iota 5219  df-fv 5263
  Copyright terms: Public domain W3C validator