Theorem fvprc 6663

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ∈ wcel 2114  ∃!weu 2653  Vcvv 3494  ∅c0 4291   class class class wbr 5066  ‘cfv 6355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-nul 5210  ax-pow 5266

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363

This theorem is referenced by:  rnfvprc  6664  dffv3  6666  fvrn0  6698  ndmfv  6700  fv2prc  6710  csbfv  6715  dffv2  6756  brfvopabrbr  6765  fvmpti  6767  fvmptnf  6790  fvmptrabfv  6799  fvunsn  6941  fvmptopab  7209  brfvopab  7211  1stval  7691  2ndval  7692  fipwuni  8890  fipwss  8893  tctr  9182  ranklim  9273  rankuni  9292  alephsing  9698  itunisuc  9841  itunitc  9843  tskmcl  10263  hashfn  13737  s1prc  13958  trclfvg  14375  trclfvcotrg  14376  strfvss  16506  strfvi  16537  setsnid  16539  elbasfv  16544  ressbas  16554  resslem  16557  firest  16706  topnval  16708  homffval  16960  comfffval  16968  oppchomfval  16984  oppcbas  16988  xpcbas  17428  lubfun  17590  glbfun  17603  oduval  17740  oduleval  17741  odumeet  17750  odujoin  17752  oduclatb  17754  ipopos  17770  isipodrs  17771  plusffval  17858  grpidval  17871  gsum0  17894  ismnd  17914  frmdplusg  18019  frmd0  18025  efmndbas  18036  efmndbasabf  18037  efmndplusg  18045  dfgrp2e  18129  grpinvfval  18142  grpinvfvalALT  18143  grpinvfvi  18146  grpsubfval  18147  grpsubfvalALT  18148  mulgfval  18226  mulgfvalALT  18227  mulgfvi  18230  cntrval  18449  cntzval  18451  cntzrcl  18457  oppgval  18475  oppgplusfval  18476  symgval  18497  symgplusg  18511  lactghmga  18533  psgnfval  18628  odfval  18660  odfvalALT  18661  oppglsm  18767  efgval  18843  mgpval  19242  mgpplusg  19243  ringidval  19253  opprval  19374  opprmulfval  19375  dvdsrval  19395  invrfval  19423  dvrfval  19434  staffval  19618  scaffval  19652  islss  19706  sralem  19949  sravsca  19954  sraip  19955  rlmval  19963  rlmsca2  19973  2idlval  20006  rrgval  20060  asclfval  20108  psrbas  20158  psr1val  20354  vr1val  20360  ply1val  20362  ply1basfvi  20409  ply1plusgfvi  20410  psr1sca2  20419  ply1sca2  20422  ply1ascl  20426  evl1fval  20491  evl1fval1  20494  zrhval  20655  zlmlem  20664  zlmvsca  20669  chrval  20672  evpmss  20730  ipffval  20792  ocvval  20811  elocv  20812  thlbas  20840  thlle  20841  thloc  20843  pjfval  20850  toponsspwpw  21530  istps  21542  tgdif0  21600  indislem  21608  txindislem  22241  fsubbas  22475  filuni  22493  ussval  22868  isusp  22870  nmfval  23198  tnglem  23249  tngds  23257  tcphval  23821  deg1fval  24674  deg1fvi  24679  uc1pval  24733  mon1pval  24735  ttglem  26662  vtxval  26785  iedgval  26786  vtxvalprc  26830  iedgvalprc  26831  edgval  26834  prcliscplgr  27196  wwlks  27613  wwlksn  27615  clwwlk  27761  clwwlkn  27804  clwwlknonmpo  27868  vafval  28380  bafval  28381  smfval  28382  vsfval  28410  resvsca  30903  resvlem  30904  prclisacycgr  32398  mvtval  32747  mexval  32749  mexval2  32750  mdvval  32751  mrsubfval  32755  msubfval  32771  elmsubrn  32775  mvhfval  32780  mpstval  32782  msrfval  32784  mstaval  32791  mclsrcl  32808  mppsval  32819  mthmval  32822  sltval2  33163  sltintdifex  33168  fvsingle  33381  funpartfv  33406  fullfunfv  33408  rankeq1o  33632  atbase  36440  llnbase  36660  lplnbase  36685  lvolbase  36729  lhpbase  37149  mzpmfp  39364  kelac1  39683  mendbas  39804  mendplusgfval  39805  mendmulrfval  39807  mendsca  39809  mendvscafval  39810  brfvimex  40396  clsneibex  40472  neicvgbex  40482  sprssspr  43663  sprsymrelfvlem  43672  prprelprb  43699  prprspr2  43700  upwlkbprop  44033