Theorem fvprc 6397

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 6396	. 2 ⊢ (¬ 𝐴 ∈ V → ¬ ∃!𝑥 𝐴𝐹𝑥)
2		tz6.12-2 6394	. 2 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅)
3	1, 2	syl 17	1 ⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1637   ∈ wcel 2156  ∃!weu 2630  Vcvv 3391  ∅c0 4116   class class class wbr 4844  ‘cfv 6097

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-nul 4983  ax-pow 5035

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ral 3101  df-rex 3102  df-rab 3105  df-v 3393  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-br 4845  df-iota 6060  df-fv 6105

This theorem is referenced by:  rnfvprc  6398  dffv3  6400  fvrn0  6432  ndmfv  6434  fv2prc  6444  csbfv  6449  dffv2  6488  brfvopabrbr  6496  fvmpti  6498  fvmptnf  6519  fvmptrabfv  6526  fvunsn  6666  fvmptopab  6923  brfvopab  6926  1stval  7396  2ndval  7397  fipwuni  8567  fipwss  8570  tctr  8859  ranklim  8950  rankuni  8969  alephsing  9379  itunisuc  9522  itunitc1  9523  itunitc  9524  tskmcl  9944  hashfn  13378  s1prc  13595  trclfvg  13975  trclfvcotrg  13976  strfvss  16087  strfvi  16120  setsnid  16122  elbasfv  16127  ressbas  16137  resslem  16140  firest  16294  topnval  16296  homffval  16550  comfffval  16558  oppchomfval  16574  oppcbas  16578  xpcbas  17019  lubfun  17181  glbfun  17194  oduval  17331  oduleval  17332  odumeet  17341  odujoin  17343  oduclatb  17345  ipopos  17361  isipodrs  17362  plusffval  17448  grpidval  17461  gsum0  17479  ismnd  17498  frmdplusg  17592  frmd0  17598  dfgrp2e  17649  grpinvfval  17661  grpinvfvi  17664  grpsubfval  17665  mulgfval  17743  mulgfvi  17746  cntrval  17949  cntzval  17951  cntzrcl  17957  oppgval  17974  oppgplusfval  17975  symgbas  17997  symgplusg  18006  lactghmga  18021  psgnfval  18117  odfval  18149  oppglsm  18254  efgval  18327  mgpval  18690  mgpplusg  18691  ringidval  18701  opprval  18822  opprmulfval  18823  dvdsrval  18843  invrfval  18871  dvrfval  18882  staffval  19047  scaffval  19081  islss  19135  sralem  19382  srasca  19386  sravsca  19387  sraip  19388  rlmval  19396  rlmsca2  19406  2idlval  19438  rrgval  19492  asclfval  19539  psrbas  19583  psr1val  19760  vr1val  19766  ply1val  19768  ply1basfvi  19815  ply1plusgfvi  19816  psr1sca2  19825  ply1sca2  19828  ply1ascl  19832  evl1fval  19896  evl1fval1  19899  zrhval  20060  zlmlem  20069  zlmvsca  20074  chrval  20077  evpmss  20135  ipffval  20199  ocvval  20218  elocv  20219  thlbas  20247  thlle  20248  thloc  20250  pjfval  20257  toponsspwpw  20937  istps  20949  tgdif0  21007  indislem  21015  txindislem  21647  fsubbas  21881  filuni  21899  ussval  22273  isusp  22275  nmfval  22603  tnglem  22654  tngds  22662  tchval  23226  deg1fval  24053  deg1fvi  24058  uc1pval  24112  mon1pval  24114  ttglem  25969  vtxval  26091  iedgval  26092  vtxvalprc  26150  iedgvalprc  26151  edgval  26154  prcliscplgr  26536  wwlks  26955  wwlksn  26957  clwwlk  27125  clwwlkn  27170  clwwlknOLD  27171  clwwlknonmpt2  27253  vafval  27785  bafval  27786  smfval  27787  vsfval  27815  resvsca  30154  resvlem  30155  mvtval  31718  mexval  31720  mexval2  31721  mdvval  31722  mrsubfval  31726  msubfval  31742  elmsubrn  31746  mvhfval  31751  mpstval  31753  msrfval  31755  mstaval  31762  mclsrcl  31779  mppsval  31790  mthmval  31793  sltval2  32128  sltintdifex  32133  fvsingle  32346  funpartfv  32371  fullfunfv  32373  rankeq1o  32597  atbase  35067  llnbase  35287  lplnbase  35312  lvolbase  35356  lhpbase  35776  mzpmfp  37809  kelac1  38131  mendbas  38252  mendplusgfval  38253  mendmulrfval  38255  mendsca  38257  mendvscafval  38258  brfvimex  38821  clsneibex  38897  neicvgbex  38907  upwlkbprop  42284  sprssspr  42296  sprsymrelfvlem  42305