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

Theorem ndmfv 5903
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 2291 . . . . 5  |-  ( E! x  A F x  ->  E. x  A F x )
2 eldmg 5047 . . . . 5  |-  ( A  e.  _V  ->  ( A  e.  dom  F  <->  E. x  A F x ) )
31, 2syl5ibr 225 . . . 4  |-  ( A  e.  _V  ->  ( E! x  A F x  ->  A  e.  dom  F ) )
43con3d 139 . . 3  |-  ( A  e.  _V  ->  ( -.  A  e.  dom  F  ->  -.  E! x  A F x ) )
5 tz6.12-2 5870 . . 3  |-  ( -.  E! x  A F x  ->  ( F `  A )  =  (/) )
64, 5syl6 35 . 2  |-  ( A  e.  _V  ->  ( -.  A  e.  dom  F  ->  ( F `  A )  =  (/) ) )
7 fvprc 5873 . . 3  |-  ( -.  A  e.  _V  ->  ( F `  A )  =  (/) )
87a1d 27 . 2  |-  ( -.  A  e.  _V  ->  ( -.  A  e.  dom  F  ->  ( F `  A )  =  (/) ) )
96, 8pm2.61i 168 1  |-  ( -.  A  e.  dom  F  ->  ( F `  A
)  =  (/) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1438   E.wex 1660    e. wcel 1869   E!weu 2266   _Vcvv 3082   (/)c0 3762   class class class wbr 4421   dom cdm 4851   ` cfv 5599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-nul 4553  ax-pow 4600
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-rab 2785  df-v 3084  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-if 3911  df-sn 3998  df-pr 4000  df-op 4004  df-uni 4218  df-br 4422  df-dm 4861  df-iota 5563  df-fv 5607
This theorem is referenced by:  ndmfvrcl  5904  elfvdm  5905  nfvres  5909  fvfundmfvn0  5911  0fv  5912  funfv  5946  fvun1  5950  fvco4i  5957  fvmpti  5961  mptrcl  5969  fvmptss  5972  fvmptex  5974  fvmptnf  5981  fvmptss2  5983  elfvmptrab1  5984  fvopab4ndm  5986  f0cli  6046  funiunfv  6166  ovprc  6333  oprssdm  6462  nssdmovg  6463  ndmovg  6464  1st2val  6831  2nd2val  6832  bropopvvv  6885  curry1val  6898  curry2val  6902  smofvon2  7081  rdgsucmptnf  7153  frsucmptn  7162  brwitnlem  7215  undifixp  7564  r1tr  8250  rankvaln  8273  cardidm  8396  carden2a  8403  carden2b  8404  carddomi2  8407  sdomsdomcardi  8408  pm54.43lem  8436  alephcard  8503  alephnbtwn  8504  alephgeom  8515  cfub  8681  cardcf  8684  cflecard  8685  cfle  8686  cflim2  8695  cfidm  8707  itunisuc  8851  itunitc1  8852  ituniiun  8854  alephadd  9004  alephreg  9009  pwcfsdom  9010  cfpwsdom  9011  adderpq  9383  mulerpq  9384  uzssz  11180  ltweuz  12176  wrdsymb0  12699  lsw0  12710  swrd00  12770  swrd0  12786  sumz  13781  sumss  13783  sumnul  13814  prod1  13991  prodss  13994  divsfval  15446  cidpropd  15608  homarcl  15916  arwval  15931  coafval  15952  lubval  16223  glbval  16236  joinval  16244  meetval  16258  gsumpropd2lem  16509  mpfrcl  18734  iscnp2  20247  setsmstopn  21485  tngtopn  21650  pcofval  22033  dvbsss  22849  perfdvf  22850  dchrrcl  24160  eleenn  24918  clwwlknprop  25492  2wlkonot3v  25595  2spthonot3v  25596  vsfval  26246  dmadjrnb  27551  hmdmadj  27585  rdgprc0  30441  soseq  30493  nofv  30545  sltres  30552  bdayelon  30568  fvnobday  30570  fullfunfv  30713  linedegen  30909  bj-inftyexpidisj  31610  dibvalrel  34656  dicvalrelN  34678  dihvalrel  34772  itgocn  35956  pfx00  38643  pfx0  38644  structiedg0val  38794  snstriedgval  38807
  Copyright terms: Public domain W3C validator