Theorem fvprc 6326

Description: A function's value at a proper class is the empty set. (Contributed by NM, 20-May-1998.)

Assertion

Ref	Expression
fvprc	⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅)

Proof of Theorem fvprc

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		brprcneu 6325	. 2 ⊢ (¬ 𝐴 ∈ V → ¬ ∃!𝑥 𝐴𝐹𝑥)
2		tz6.12-2 6323	. 2 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅)
3	1, 2	syl 17	1 ⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1631   ∈ wcel 2145  ∃!weu 2618  Vcvv 3351  ∅c0 4063   class class class wbr 4786  ‘cfv 6031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-nul 4923  ax-pow 4974

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-iota 5994  df-fv 6039

This theorem is referenced by:  dffv3  6328  fvrn0  6357  ndmfv  6359  fv2prc  6369  csbfv  6374  dffv2  6413  brfvopabrbr  6421  fvmpti  6423  fvmptnf  6444  fvmptrabfv  6451  fvunsn  6589  fvmptopab  6844  brfvopab  6847  1stval  7317  2ndval  7318  fipwuni  8488  fipwss  8491  tctr  8780  ranklim  8871  rankuni  8890  alephsing  9300  itunisuc  9443  itunitc1  9444  itunitc  9445  tskmcl  9865  hashfn  13366  s1prc  13584  trclfvg  13964  trclfvcotrg  13965  strfvss  16087  strfvi  16120  setsnid  16122  elbasfv  16127  ressbas  16137  resslem  16140  firest  16301  topnval  16303  homffval  16557  comfffval  16565  oppchomfval  16581  oppcbas  16585  xpcbas  17026  lubfun  17188  glbfun  17201  oduval  17338  oduleval  17339  odumeet  17348  odujoin  17350  oduclatb  17352  ipopos  17368  isipodrs  17369  plusffval  17455  grpidval  17468  gsum0  17486  ismnd  17505  frmdplusg  17599  frmd0  17605  dfgrp2e  17656  grpinvfval  17668  grpinvfvi  17671  grpsubfval  17672  mulgfval  17750  mulgfvi  17753  cntrval  17959  cntzval  17961  cntzrcl  17967  oppgval  17984  oppgplusfval  17985  symgbas  18007  symgplusg  18016  lactghmga  18031  pmtrfrn  18085  psgnfval  18127  odfval  18159  oppglsm  18264  efgval  18337  mgpval  18700  mgpplusg  18701  ringidval  18711  opprval  18832  opprmulfval  18833  dvdsrval  18853  invrfval  18881  dvrfval  18892  staffval  19057  scaffval  19091  islss  19145  sralem  19392  srasca  19396  sravsca  19397  sraip  19398  rlmval  19406  rlmsca2  19416  2idlval  19448  rrgval  19502  asclfval  19549  psrbas  19593  psr1val  19771  vr1val  19777  ply1val  19779  ply1basfvi  19826  ply1plusgfvi  19827  psr1sca2  19836  ply1sca2  19839  ply1ascl  19843  evl1fval  19907  evl1fval1  19910  zrhval  20071  zlmlem  20080  zlmvsca  20085  chrval  20088  evpmss  20147  ipffval  20210  ocvval  20228  elocv  20229  thlbas  20257  thlle  20258  thloc  20260  pjfval  20267  toponsspwpw  20947  istps  20959  tgdif0  21017  indislem  21025  txindislem  21657  fsubbas  21891  filuni  21909  ussval  22283  isusp  22285  nmfval  22613  tnglem  22664  tngds  22672  tchval  23236  deg1fval  24060  deg1fvi  24065  uc1pval  24119  mon1pval  24121  ttglem  25977  vtxval  26099  iedgval  26100  vtxvalprc  26158  iedgvalprc  26159  edgval  26162  prcliscplgr  26544  wwlks  26963  wwlksn  26965  clwwlk  27133  clwwlkn  27178  clwwlknOLD  27179  clwwlknonmpt2  27261  vafval  27798  bafval  27799  smfval  27800  vsfval  27828  resvsca  30170  resvlem  30171  mvtval  31735  mexval  31737  mexval2  31738  mdvval  31739  mrsubfval  31743  mrsubrn  31748  mrsub0  31751  mrsubf  31752  mrsubccat  31753  mrsubcn  31754  mrsubco  31756  mrsubvrs  31757  msubfval  31759  elmsubrn  31763  msubrn  31764  msubf  31767  mvhfval  31768  mpstval  31770  msrfval  31772  mstaval  31779  mclsrcl  31796  mppsval  31807  mthmval  31810  sltval2  32146  sltintdifex  32151  fvsingle  32364  funpartfv  32389  fullfunfv  32391  rankeq1o  32615  atbase  35098  llnbase  35317  lplnbase  35342  lvolbase  35386  lhpbase  35806  mzpmfp  37836  kelac1  38159  mendbas  38280  mendplusgfval  38281  mendmulrfval  38283  mendsca  38285  mendvscafval  38286  brfvimex  38850  clsneibex  38926  neicvgbex  38936  upwlkbprop  42247  sprssspr  42259  sprsymrelfvlem  42268