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

Theorem fvprc 5519
Description: A function's value at a proper class is the empty set. (Contributed by NM, 20-May-1998.)
Assertion
Ref Expression
fvprc  |-  ( -.  A  e.  _V  ->  ( F `  A )  =  (/) )

Proof of Theorem fvprc
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 brprcneu 5518 . 2  |-  ( -.  A  e.  _V  ->  -.  E! x  A F x )
2 tz6.12-2 5516 . 2  |-  ( -.  E! x  A F x  ->  ( F `  A )  =  (/) )
31, 2syl 15 1  |-  ( -.  A  e.  _V  ->  ( F `  A )  =  (/) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1623    e. wcel 1684   E!weu 2143   _Vcvv 2788   (/)c0 3455   class class class wbr 4023   ` cfv 5255
This theorem is referenced by:  dffv3  5521  fvrn0  5550  ndmfv  5552  dffv2  5592  fvmpti  5601  fvmptnf  5617  fvunsn  5712  1stval  6124  2ndval  6125  riotav  6309  riotaprc  6342  riotassuni  6343  fipwuni  7179  fipwss  7182  tctr  7425  ranklim  7516  rankuni  7535  alephsing  7902  itunisuc  8045  itunitc1  8046  itunitc  8047  tskmcl  8463  hashfn  11357  strfvss  13166  strfvi  13186  setsnid  13188  elbasfv  13191  ressbas  13198  resslem  13201  firest  13337  topnval  13339  homffval  13594  comfffval  13601  oppchomfval  13617  oppcbas  13621  xpcbas  13952  oduval  14234  oduleval  14235  odumeet  14244  odujoin  14246  oduclatb  14248  ipopos  14263  isipodrs  14264  ismnd  14369  plusffval  14379  grpidval  14384  gsum0  14457  frmdplusg  14476  frmd0  14482  grpinvfval  14520  grpinvfvi  14523  grpsubfval  14524  mulgfval  14568  mulgfvi  14571  symgbas  14772  symgplusg  14776  lactghmga  14784  cntrval  14795  cntzval  14797  cntzrcl  14803  oppgval  14820  oppgplusfval  14821  odfval  14848  oppglsm  14953  efgval  15026  mgpval  15328  mgpplusg  15329  rngidval  15343  opprval  15406  opprmulfval  15407  dvdsrval  15427  invrfval  15455  dvrfval  15466  staffval  15612  scaffval  15645  islss  15692  sralem  15930  srasca  15934  sravsca  15935  rlmval  15945  rlmsca2  15953  2idlval  15985  rrgval  16028  asclfval  16074  psrbas  16124  psr1val  16265  vr1val  16271  ply1val  16273  psr1rclOLD  16279  ply1rclOLD  16282  ply1basfvi  16319  ply1plusgfvi  16320  psr1sca2  16329  ply1sca2  16332  ply1ascl  16335  zrhval  16462  zlmlem  16471  zlmvsca  16476  chrval  16479  ipffval  16552  ocvval  16567  elocv  16568  thlbas  16596  thlle  16597  thloc  16599  pjfval  16606  istps  16674  tgclb  16708  tgdif0  16730  indislem  16737  txindislem  17327  fsubbas  17562  filuni  17580  nmfval  18111  tnglem  18156  tngds  18164  tchval  18650  evl1fval  19410  deg1fval  19466  deg1fvi  19471  uc1pval  19525  mon1pval  19527  vafval  21159  bafval  21160  smfval  21161  vsfval  21191  sltval2  24310  sltintdifex  24317  fullfunfv  24485  rankeq1o  24801  domval  25723  codval  25724  idval  25725  cmpval  25726  mzpmfp  26825  kelac1  27161  pmtrfrn  27400  psgnfval  27423  mendbas  27492  mendplusgfval  27493  mendmulrfval  27495  mendsca  27497  mendvscafval  27498  atbase  29479  llnbase  29698  lplnbase  29723  lvolbase  29767  lhpbase  30187
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-nul 4149  ax-pow 4188
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263
  Copyright terms: Public domain W3C validator