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

Theorem fvprc 5792
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 5791 . 2  |-  ( -.  A  e.  _V  ->  -.  E! x  A F x )
2 tz6.12-2 5789 . 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 1370    e. wcel 1758   E!weu 2262   _Vcvv 3076   (/)c0 3744   class class class wbr 4399   ` cfv 5525
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-nul 4528  ax-pow 4577
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-ral 2803  df-rex 2804  df-rab 2807  df-v 3078  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-sn 3985  df-pr 3987  df-op 3991  df-uni 4199  df-br 4400  df-iota 5488  df-fv 5533
This theorem is referenced by:  dffv3  5794  fvrn0  5820  ndmfv  5822  csbfv  5836  dffv2  5872  fvmpti  5881  fvmptnf  5899  fvunsn  6018  1stval  6688  2ndval  6689  fipwuni  7786  fipwss  7789  tctr  8070  ranklim  8161  rankuni  8180  alephsing  8555  itunisuc  8698  itunitc1  8699  itunitc  8700  tskmcl  9118  hashfn  12255  strfvss  14309  strfvi  14331  setsnid  14333  elbasfv  14338  ressbas  14346  resslem  14349  firest  14489  topnval  14491  homffval  14748  comfffval  14755  oppchomfval  14771  oppcbas  14775  xpcbas  15106  lubfun  15268  glbfun  15281  oduval  15418  oduleval  15419  odumeet  15428  odujoin  15430  oduclatb  15432  ipopos  15448  isipodrs  15449  ismnd  15535  plusffval  15545  grpidval  15550  gsum0  15628  frmdplusg  15650  frmd0  15656  grpinvfval  15694  grpinvfvi  15697  grpsubfval  15698  mulgfval  15746  mulgfvi  15749  cntrval  15955  cntzval  15957  cntzrcl  15963  oppgval  15980  oppgplusfval  15981  symgbas  16003  symgplusg  16012  lactghmga  16027  pmtrfrn  16082  psgnfval  16124  odfval  16156  oppglsm  16261  efgval  16334  mgpval  16715  mgpplusg  16716  rngidval  16726  opprval  16838  opprmulfval  16839  dvdsrval  16859  invrfval  16887  dvrfval  16898  staffval  17054  scaffval  17088  islss  17138  sralem  17380  srasca  17384  sravsca  17385  sraip  17386  rlmval  17394  rlmsca2  17404  2idlval  17437  rrgval  17480  asclfval  17527  psrbas  17570  psrbasOLD  17571  psr1val  17765  vr1val  17771  ply1val  17773  ply1basfvi  17818  ply1plusgfvi  17819  psr1sca2  17828  ply1sca2  17831  ply1ascl  17834  evl1fval  17886  evl1fval1  17889  zrhval  18063  zlmlem  18072  zlmvsca  18077  chrval  18080  evpmss  18140  ipffval  18201  ocvval  18216  elocv  18217  thlbas  18245  thlle  18246  thloc  18248  pjfval  18255  istps  18672  tgdif0  18728  indislem  18735  txindislem  19337  fsubbas  19571  filuni  19589  ussval  19965  isusp  19967  nmfval  20312  tnglem  20357  tngds  20365  tchval  20864  deg1fval  21683  deg1fvi  21688  uc1pval  21743  mon1pval  21745  ttglem  23273  vafval  24132  bafval  24133  smfval  24134  vsfval  24164  resvsca  26442  resvlem  26443  sltval2  27940  sltintdifex  27947  fvsingle  28094  funpartfv  28119  fullfunfv  28121  rankeq1o  28352  mzpmfp  29230  mzpmfpOLD  29231  kelac1  29563  mendbas  29688  mendplusgfval  29689  mendmulrfval  29691  mendsca  29693  mendvscafval  29694  atbase  33257  llnbase  33476  lplnbase  33501  lvolbase  33545  lhpbase  33965
  Copyright terms: Public domain W3C validator