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

Theorem fvprc 5860
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 5859 . 2  |-  ( -.  A  e.  _V  ->  -.  E! x  A F x )
2 tz6.12-2 5857 . 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 1379    e. wcel 1767   E!weu 2275   _Vcvv 3113   (/)c0 3785   class class class wbr 4447   ` cfv 5588
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-nul 4576  ax-pow 4625
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-iota 5551  df-fv 5596
This theorem is referenced by:  dffv3  5862  fvrn0  5888  ndmfv  5890  csbfv  5904  dffv2  5940  fvmpti  5949  fvmptnf  5967  fvunsn  6093  1stval  6786  2ndval  6787  fipwuni  7886  fipwss  7889  tctr  8171  ranklim  8262  rankuni  8281  alephsing  8656  itunisuc  8799  itunitc1  8800  itunitc  8801  tskmcl  9219  hashfn  12411  strfvss  14508  strfvi  14530  setsnid  14532  elbasfv  14537  ressbas  14545  resslem  14548  firest  14688  topnval  14690  homffval  14947  comfffval  14954  oppchomfval  14970  oppcbas  14974  xpcbas  15305  lubfun  15467  glbfun  15480  oduval  15617  oduleval  15618  odumeet  15627  odujoin  15629  oduclatb  15631  ipopos  15647  isipodrs  15648  ismnd  15734  plusffval  15744  grpidval  15749  gsum0  15832  frmdplusg  15854  frmd0  15860  grpinvfval  15898  grpinvfvi  15901  grpsubfval  15902  mulgfval  15953  mulgfvi  15956  cntrval  16162  cntzval  16164  cntzrcl  16170  oppgval  16187  oppgplusfval  16188  symgbas  16210  symgplusg  16219  lactghmga  16234  pmtrfrn  16289  psgnfval  16331  odfval  16363  oppglsm  16468  efgval  16541  mgpval  16946  mgpplusg  16947  rngidval  16957  opprval  17074  opprmulfval  17075  dvdsrval  17095  invrfval  17123  dvrfval  17134  staffval  17296  scaffval  17330  islss  17381  sralem  17623  srasca  17627  sravsca  17628  sraip  17629  rlmval  17637  rlmsca2  17647  2idlval  17680  rrgval  17734  asclfval  17782  psrbas  17829  psrbasOLD  17830  psr1val  18024  vr1val  18030  ply1val  18032  ply1basfvi  18081  ply1plusgfvi  18082  psr1sca2  18091  ply1sca2  18094  ply1ascl  18098  evl1fval  18163  evl1fval1  18166  zrhval  18340  zlmlem  18349  zlmvsca  18354  chrval  18357  evpmss  18417  ipffval  18478  ocvval  18493  elocv  18494  thlbas  18522  thlle  18523  thloc  18525  pjfval  18532  istps  19232  tgdif0  19288  indislem  19295  txindislem  19897  fsubbas  20131  filuni  20149  ussval  20525  isusp  20527  nmfval  20872  tnglem  20917  tngds  20925  tchval  21424  deg1fval  22243  deg1fvi  22248  uc1pval  22303  mon1pval  22305  ttglem  23883  vafval  25200  bafval  25201  smfval  25202  vsfval  25232  resvsca  27511  resvlem  27512  sltval2  29021  sltintdifex  29028  fvsingle  29175  funpartfv  29200  fullfunfv  29202  rankeq1o  29433  mzpmfp  30311  mzpmfpOLD  30312  kelac1  30641  mendbas  30766  mendplusgfval  30767  mendmulrfval  30769  mendsca  30771  mendvscafval  30772  atbase  34104  llnbase  34323  lplnbase  34348  lvolbase  34392  lhpbase  34812
  Copyright terms: Public domain W3C validator