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

Theorem ndmfv 5719
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 2281 . . . . 5  |-  ( E! x  A F x  ->  E. x  A F x )
2 eldmg 5040 . . . . 5  |-  ( A  e.  _V  ->  ( A  e.  dom  F  <->  E. x  A F x ) )
31, 2syl5ibr 221 . . . 4  |-  ( A  e.  _V  ->  ( E! x  A F x  ->  A  e.  dom  F ) )
43con3d 133 . . 3  |-  ( A  e.  _V  ->  ( -.  A  e.  dom  F  ->  -.  E! x  A F x ) )
5 tz6.12-2 5687 . . 3  |-  ( -.  E! x  A F x  ->  ( F `  A )  =  (/) )
64, 5syl6 33 . 2  |-  ( A  e.  _V  ->  ( -.  A  e.  dom  F  ->  ( F `  A )  =  (/) ) )
7 fvprc 5690 . . 3  |-  ( -.  A  e.  _V  ->  ( F `  A )  =  (/) )
87a1d 25 . 2  |-  ( -.  A  e.  _V  ->  ( -.  A  e.  dom  F  ->  ( F `  A )  =  (/) ) )
96, 8pm2.61i 164 1  |-  ( -.  A  e.  dom  F  ->  ( F `  A
)  =  (/) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1369   E.wex 1586    e. wcel 1756   E!weu 2253   _Vcvv 2977   (/)c0 3642   class class class wbr 4297   dom cdm 4845   ` cfv 5423
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-nul 4426  ax-pow 4475
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ne 2613  df-ral 2725  df-rex 2726  df-rab 2729  df-v 2979  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-nul 3643  df-if 3797  df-sn 3883  df-pr 3885  df-op 3889  df-uni 4097  df-br 4298  df-dm 4855  df-iota 5386  df-fv 5431
This theorem is referenced by:  ndmfvrcl  5720  elfvdm  5721  nfvres  5725  fvfundmfvn0  5727  0fv  5728  funfv  5763  fvun1  5767  fvco4i  5774  fvmpti  5778  fvmptss  5787  fvmptex  5789  fvmptnf  5796  fvmptss2  5798  fvopab4ndm  5799  f0cli  5859  funiunfv  5970  ovprc  6123  oprssdm  6249  nssdmovg  6250  ndmovg  6251  1st2val  6607  2nd2val  6608  bropopvvv  6658  curry1val  6670  curry2val  6674  smofvon2  6822  rdgsucmptnf  6890  frsucmptn  6899  brwitnlem  6952  undifixp  7304  r1tr  7988  rankvaln  8011  cardidm  8134  carden2a  8141  carden2b  8142  carddomi2  8145  sdomsdomcardi  8146  pm54.43lem  8174  alephcard  8245  alephnbtwn  8246  alephgeom  8257  cfub  8423  cardcf  8426  cflecard  8427  cfle  8428  cflim2  8437  cfidm  8449  itunisuc  8593  itunitc1  8594  ituniiun  8596  alephadd  8746  alephreg  8751  pwcfsdom  8752  cfpwsdom  8753  adderpq  9130  mulerpq  9131  uzssz  10885  ltweuz  11789  wrdsymb0  12264  lsw0  12272  swrd00  12319  swrd0  12332  sumz  13204  sumss  13206  sumnul  13232  divsfval  14490  cidpropd  14654  homarcl  14901  arwval  14916  coafval  14937  lubval  15159  glbval  15172  joinval  15180  meetval  15194  gsumpropd2lem  15510  mpfrcl  17609  iscnp2  18848  setsmstopn  20058  tngtopn  20241  pcofval  20587  dvbsss  21382  perfdvf  21383  dchrrcl  22584  eleenn  23147  vsfval  24018  dmadjrnb  25315  hmdmadj  25349  prod1  27462  prodss  27465  rdgprc0  27612  soseq  27720  nofv  27803  sltres  27810  bdayelon  27826  fvnobday  27828  fullfunfv  27983  linedegen  28179  itgocn  29526  elfvmptrab1  30159  2wlkonot3v  30399  2spthonot3v  30400  clwwlknprop  30440  bj-inftyexpidisj  32538  dibvalrel  34813  dicvalrelN  34835  dihvalrel  34929
  Copyright terms: Public domain W3C validator