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

Theorem ndmfv 5872
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 2310 . . . . 5  |-  ( E! x  A F x  ->  E. x  A F x )
2 eldmg 5187 . . . . 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 5839 . . 3  |-  ( -.  E! x  A F x  ->  ( F `  A )  =  (/) )
64, 5syl6 33 . 2  |-  ( A  e.  _V  ->  ( -.  A  e.  dom  F  ->  ( F `  A )  =  (/) ) )
7 fvprc 5842 . . 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 1398   E.wex 1617    e. wcel 1823   E!weu 2284   _Vcvv 3106   (/)c0 3783   class class class wbr 4439   dom cdm 4988   ` cfv 5570
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-nul 4568  ax-pow 4615
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-dm 4998  df-iota 5534  df-fv 5578
This theorem is referenced by:  ndmfvrcl  5873  elfvdm  5874  nfvres  5878  fvfundmfvn0  5880  0fv  5881  funfv  5915  fvun1  5919  fvco4i  5926  fvmpti  5930  mptrcl  5937  fvmptss  5940  fvmptex  5942  fvmptnf  5949  fvmptss2  5951  elfvmptrab1  5952  fvopab4ndm  5954  f0cli  6018  funiunfv  6135  ovprc  6300  oprssdm  6429  nssdmovg  6430  ndmovg  6431  1st2val  6799  2nd2val  6800  bropopvvv  6853  curry1val  6866  curry2val  6870  smofvon2  7019  rdgsucmptnf  7087  frsucmptn  7096  brwitnlem  7149  undifixp  7498  r1tr  8185  rankvaln  8208  cardidm  8331  carden2a  8338  carden2b  8339  carddomi2  8342  sdomsdomcardi  8343  pm54.43lem  8371  alephcard  8442  alephnbtwn  8443  alephgeom  8454  cfub  8620  cardcf  8623  cflecard  8624  cfle  8625  cflim2  8634  cfidm  8646  itunisuc  8790  itunitc1  8791  ituniiun  8793  alephadd  8943  alephreg  8948  pwcfsdom  8949  cfpwsdom  8950  adderpq  9323  mulerpq  9324  uzssz  11101  ltweuz  12054  wrdsymb0  12563  lsw0  12574  swrd00  12634  swrd0  12650  sumz  13626  sumss  13628  sumnul  13657  prod1  13833  prodss  13836  divsfval  15036  cidpropd  15198  homarcl  15506  arwval  15521  coafval  15542  lubval  15813  glbval  15826  joinval  15834  meetval  15848  gsumpropd2lem  16099  mpfrcl  18382  iscnp2  19907  setsmstopn  21147  tngtopn  21330  pcofval  21676  dvbsss  22472  perfdvf  22473  dchrrcl  23713  eleenn  24401  clwwlknprop  24974  2wlkonot3v  25077  2spthonot3v  25078  vsfval  25726  dmadjrnb  27023  hmdmadj  27057  rdgprc0  29466  soseq  29574  nofv  29657  sltres  29664  bdayelon  29680  fvnobday  29682  fullfunfv  29825  linedegen  30021  itgocn  31354  pfx00  32612  pfx0  32613  bj-inftyexpidisj  35013  dibvalrel  37287  dicvalrelN  37309  dihvalrel  37403
  Copyright terms: Public domain W3C validator