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

Theorem ndmfv 5554
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 2168 . . . . 5  |-  ( E! x  A F x  ->  E. x  A F x )
2 eldmg 4876 . . . . 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 5518 . . 3  |-  ( -.  E! x  A F x  ->  ( F `  A )  =  (/) )
64, 5syl6 29 . 2  |-  ( A  e.  _V  ->  ( -.  A  e.  dom  F  ->  ( F `  A )  =  (/) ) )
7 fvprc 5521 . . 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 1530    = wceq 1625    e. wcel 1686   E!weu 2145   _Vcvv 2790   (/)c0 3457   class class class wbr 4025   dom cdm 4691   ` cfv 5257
This theorem is referenced by:  ndmfvrcl  5555  elfvdm  5556  nfvres  5559  fv01  5561  funfv  5588  fvun1  5592  fvco4i  5599  fvmpti  5603  fvmptss  5611  fvmptex  5612  fvmptnf  5619  fvmptss2  5621  fvopab4ndm  5622  f0cli  5673  funiunfv  5776  ovprc  5887  oprssdm  6004  ndmovg  6005  1st2val  6147  2nd2val  6148  curry1val  6213  curry2val  6217  smofvon2  6375  rdgsucmptnf  6444  frsucmptn  6453  brwitnlem  6508  undifixp  6854  r1tr  7450  rankvaln  7473  cardidm  7594  carden2a  7601  carden2b  7602  carddomi2  7605  sdomsdomcardi  7606  pm54.43lem  7634  alephcard  7699  alephnbtwn  7700  alephgeom  7711  cfub  7877  cardcf  7880  cflecard  7881  cfle  7882  cflim2  7891  cfidm  7903  itunisuc  8047  itunitc1  8048  ituniiun  8050  alephadd  8201  alephreg  8206  pwcfsdom  8207  cfpwsdom  8208  adderpq  8582  mulerpq  8583  uzssz  10249  ltweuz  11026  swrd00  11453  sumz  12197  sumss  12199  sumnul  12225  divsfval  13451  cidpropd  13615  homarcl  13862  arwval  13877  coafval  13898  iscnp2  16971  setsmstopn  18026  tngtopn  18168  pcofval  18510  dvbsss  19254  perfdvf  19255  mpfrcl  19404  dchrrcl  20481  vsfval  21193  dmadjrnb  22488  hmdmadj  22522  gsumpropd2lem  23381  rdgprc0  24152  soseq  24256  nofv  24313  sltres  24320  bdayelon  24336  fvnobday  24338  fullfunfv  24487  eleenn  24526  linedegen  24768  fvsnn  25125  itgocn  27380  matrcl  27477  fvfundmfvn0  27997  nssdmovg  28088  dibvalrel  31426  dicvalrelN  31448  dihvalrel  31542
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-nul 4151  ax-pow 4190
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-uni 3830  df-br 4026  df-dm 4701  df-iota 5221  df-fv 5265
  Copyright terms: Public domain W3C validator