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

Theorem ndmfv 5911
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 2333 . . . . 5  |-  ( E! x  A F x  ->  E. x  A F x )
2 eldmg 5048 . . . . 5  |-  ( A  e.  _V  ->  ( A  e.  dom  F  <->  E. x  A F x ) )
31, 2syl5ibr 229 . . . 4  |-  ( A  e.  _V  ->  ( E! x  A F x  ->  A  e.  dom  F ) )
43con3d 140 . . 3  |-  ( A  e.  _V  ->  ( -.  A  e.  dom  F  ->  -.  E! x  A F x ) )
5 tz6.12-2 5878 . . 3  |-  ( -.  E! x  A F x  ->  ( F `  A )  =  (/) )
64, 5syl6 34 . 2  |-  ( A  e.  _V  ->  ( -.  A  e.  dom  F  ->  ( F `  A )  =  (/) ) )
7 fvprc 5881 . . 3  |-  ( -.  A  e.  _V  ->  ( F `  A )  =  (/) )
87a1d 26 . 2  |-  ( -.  A  e.  _V  ->  ( -.  A  e.  dom  F  ->  ( F `  A )  =  (/) ) )
96, 8pm2.61i 169 1  |-  ( -.  A  e.  dom  F  ->  ( F `  A
)  =  (/) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1454   E.wex 1673    e. wcel 1897   E!weu 2309   _Vcvv 3056   (/)c0 3742   class class class wbr 4415   dom cdm 4852   ` cfv 5600
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-nul 4547  ax-pow 4594
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-ral 2753  df-rex 2754  df-rab 2757  df-v 3058  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986  df-uni 4212  df-br 4416  df-dm 4862  df-iota 5564  df-fv 5608
This theorem is referenced by:  ndmfvrcl  5912  elfvdm  5913  nfvres  5917  fvfundmfvn0  5919  0fv  5920  funfv  5954  fvun1  5958  fvco4i  5965  fvmpti  5969  mptrcl  5977  fvmptss  5980  fvmptex  5982  fvmptnf  5989  fvmptss2  5991  elfvmptrab1  5992  fvopab4ndm  5994  f0cli  6055  funiunfv  6177  ovprc  6344  oprssdm  6476  nssdmovg  6477  ndmovg  6478  1st2val  6845  2nd2val  6846  brovpreldm  6899  curry1val  6915  curry2val  6919  smofvon2  7100  rdgsucmptnf  7172  frsucmptn  7181  brwitnlem  7234  undifixp  7583  r1tr  8272  rankvaln  8295  cardidm  8418  carden2a  8425  carden2b  8426  carddomi2  8429  sdomsdomcardi  8430  pm54.43lem  8458  alephcard  8526  alephnbtwn  8527  alephgeom  8538  cfub  8704  cardcf  8707  cflecard  8708  cfle  8709  cflim2  8718  cfidm  8730  itunisuc  8874  itunitc1  8875  ituniiun  8877  alephadd  9027  alephreg  9032  pwcfsdom  9033  cfpwsdom  9034  adderpq  9406  mulerpq  9407  uzssz  11206  ltweuz  12206  wrdsymb0  12736  lsw0  12747  swrd00  12810  swrd0  12826  sumz  13836  sumss  13838  sumnul  13869  prod1  14046  prodss  14049  divsfval  15501  cidpropd  15663  homarcl  15971  arwval  15986  coafval  16007  lubval  16278  glbval  16291  joinval  16299  meetval  16313  gsumpropd2lem  16564  mpfrcl  18789  iscnp2  20303  setsmstopn  21541  tngtopn  21706  pcofval  22089  dvbsss  22905  perfdvf  22906  dchrrcl  24216  eleenn  24974  clwwlknprop  25548  2wlkonot3v  25651  2spthonot3v  25652  vsfval  26302  dmadjrnb  27607  hmdmadj  27641  rdgprc0  30488  soseq  30540  nofv  30592  sltres  30599  noseponlem  30603  bdayelon  30617  fvnobday  30619  fullfunfv  30762  linedegen  30958  bj-inftyexpidisj  31696  dibvalrel  34775  dicvalrelN  34797  dihvalrel  34891  itgocn  36074  pfx00  38964  pfx0  38965  structiedg0val  39169  snstriedgval  39183  rgrx0nd  39658
  Copyright terms: Public domain W3C validator