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

Theorem fvprc 5673
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 5672 . 2  |-  ( -.  A  e.  _V  ->  -.  E! x  A F x )
2 tz6.12-2 5670 . 2  |-  ( -.  E! x  A F x  ->  ( F `  A )  =  (/) )
31, 2syl 16 1  |-  ( -.  A  e.  _V  ->  ( F `  A )  =  (/) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1362    e. wcel 1755   E!weu 2254   _Vcvv 2962   (/)c0 3625   class class class wbr 4280   ` cfv 5406
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-nul 4409  ax-pow 4458
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-iota 5369  df-fv 5414
This theorem is referenced by:  dffv3  5675  fvrn0  5700  ndmfv  5702  csbfv  5716  dffv2  5752  fvmpti  5761  fvmptnf  5779  fvunsn  5897  1stval  6568  2ndval  6569  fipwuni  7664  fipwss  7667  tctr  7948  ranklim  8039  rankuni  8058  alephsing  8433  itunisuc  8576  itunitc1  8577  itunitc  8578  tskmcl  8995  hashfn  12121  strfvss  14174  strfvi  14196  setsnid  14198  elbasfv  14203  ressbas  14210  resslem  14213  firest  14353  topnval  14355  homffval  14612  comfffval  14619  oppchomfval  14635  oppcbas  14639  xpcbas  14970  lubfun  15132  glbfun  15145  oduval  15282  oduleval  15283  odumeet  15292  odujoin  15294  oduclatb  15296  ipopos  15312  isipodrs  15313  ismnd  15399  plusffval  15409  grpidval  15414  gsum0  15489  frmdplusg  15511  frmd0  15517  grpinvfval  15555  grpinvfvi  15558  grpsubfval  15559  mulgfval  15607  mulgfvi  15610  cntrval  15816  cntzval  15818  cntzrcl  15824  oppgval  15841  oppgplusfval  15842  symgbas  15864  symgplusg  15873  lactghmga  15888  pmtrfrn  15943  psgnfval  15985  odfval  16015  oppglsm  16120  efgval  16193  mgpval  16567  mgpplusg  16568  rngidval  16582  opprval  16649  opprmulfval  16650  dvdsrval  16670  invrfval  16698  dvrfval  16709  staffval  16855  scaffval  16889  islss  16937  sralem  17179  srasca  17183  sravsca  17184  sraip  17185  rlmval  17193  rlmsca2  17203  2idlval  17236  rrgval  17279  asclfval  17326  psrbas  17381  psrbasOLD  17382  psr1val  17540  vr1val  17546  ply1val  17548  ply1basfvi  17593  ply1plusgfvi  17594  psr1sca2  17603  ply1sca2  17606  ply1ascl  17609  zrhval  17780  zlmlem  17789  zlmvsca  17794  chrval  17797  evpmss  17857  ipffval  17918  ocvval  17933  elocv  17934  thlbas  17962  thlle  17963  thloc  17965  pjfval  17972  istps  18382  tgdif0  18438  indislem  18445  txindislem  19047  fsubbas  19281  filuni  19299  ussval  19675  isusp  19677  nmfval  20022  tnglem  20067  tngds  20075  tchval  20574  evl1fval  21377  deg1fval  21435  deg1fvi  21440  uc1pval  21495  mon1pval  21497  ttglem  22944  vafval  23803  bafval  23804  smfval  23805  vsfval  23835  resvsca  26151  resvlem  26152  sltval2  27643  sltintdifex  27650  fvsingle  27797  funpartfv  27822  fullfunfv  27824  rankeq1o  28055  mzpmfp  28925  mzpmfpOLD  28926  kelac1  29258  mendbas  29383  mendplusgfval  29384  mendmulrfval  29386  mendsca  29388  mendvscafval  29389  atbase  32504  llnbase  32723  lplnbase  32748  lvolbase  32792  lhpbase  33212
  Copyright terms: Public domain W3C validator