Theorem fvprc 6658

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1533   ∈ wcel 2110  ∃!weu 2649  Vcvv 3495  ∅c0 4291   class class class wbr 5059  ‘cfv 6350

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-nul 5203  ax-pow 5259

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4833  df-br 5060  df-iota 6309  df-fv 6358

This theorem is referenced by:  rnfvprc  6659  dffv3  6661  fvrn0  6693  ndmfv  6695  fv2prc  6705  csbfv  6710  dffv2  6751  brfvopabrbr  6760  fvmpti  6762  fvmptnf  6785  fvmptrabfv  6794  fvunsn  6936  fvmptopab  7203  brfvopab  7205  1stval  7685  2ndval  7686  fipwuni  8884  fipwss  8887  tctr  9176  ranklim  9267  rankuni  9286  alephsing  9692  itunisuc  9835  itunitc  9837  tskmcl  10257  hashfn  13730  s1prc  13952  trclfvg  14369  trclfvcotrg  14370  strfvss  16500  strfvi  16531  setsnid  16533  elbasfv  16538  ressbas  16548  resslem  16551  firest  16700  topnval  16702  homffval  16954  comfffval  16962  oppchomfval  16978  oppcbas  16982  xpcbas  17422  lubfun  17584  glbfun  17597  oduval  17734  oduleval  17735  odumeet  17744  odujoin  17746  oduclatb  17748  ipopos  17764  isipodrs  17765  plusffval  17852  grpidval  17865  gsum0  17888  ismnd  17908  frmdplusg  18013  frmd0  18019  efmndbas  18030  efmndbasabf  18031  efmndplusg  18039  dfgrp2e  18123  grpinvfval  18136  grpinvfvalALT  18137  grpinvfvi  18140  grpsubfval  18141  grpsubfvalALT  18142  mulgfval  18220  mulgfvalALT  18221  mulgfvi  18224  cntrval  18443  cntzval  18445  cntzrcl  18451  oppgval  18469  oppgplusfval  18470  symgval  18491  symgplusg  18505  lactghmga  18527  psgnfval  18622  odfval  18654  odfvalALT  18655  oppglsm  18761  efgval  18837  mgpval  19236  mgpplusg  19237  ringidval  19247  opprval  19368  opprmulfval  19369  dvdsrval  19389  invrfval  19417  dvrfval  19428  staffval  19612  scaffval  19646  islss  19700  sralem  19943  sravsca  19948  sraip  19949  rlmval  19957  rlmsca2  19967  2idlval  20000  rrgval  20054  asclfval  20102  psrbas  20152  psr1val  20348  vr1val  20354  ply1val  20356  ply1basfvi  20403  ply1plusgfvi  20404  psr1sca2  20413  ply1sca2  20416  ply1ascl  20420  evl1fval  20485  evl1fval1  20488  zrhval  20649  zlmlem  20658  zlmvsca  20663  chrval  20666  evpmss  20724  ipffval  20786  ocvval  20805  elocv  20806  thlbas  20834  thlle  20835  thloc  20837  pjfval  20844  toponsspwpw  21524  istps  21536  tgdif0  21594  indislem  21602  txindislem  22235  fsubbas  22469  filuni  22487  ussval  22862  isusp  22864  nmfval  23192  tnglem  23243  tngds  23251  tcphval  23815  deg1fval  24668  deg1fvi  24673  uc1pval  24727  mon1pval  24729  ttglem  26656  vtxval  26779  iedgval  26780  vtxvalprc  26824  iedgvalprc  26825  edgval  26828  prcliscplgr  27190  wwlks  27607  wwlksn  27609  clwwlk  27755  clwwlkn  27798  clwwlknonmpo  27862  vafval  28374  bafval  28375  smfval  28376  vsfval  28404  resvsca  30898  resvlem  30899  prclisacycgr  32393  mvtval  32742  mexval  32744  mexval2  32745  mdvval  32746  mrsubfval  32750  msubfval  32766  elmsubrn  32770  mvhfval  32775  mpstval  32777  msrfval  32779  mstaval  32786  mclsrcl  32803  mppsval  32814  mthmval  32817  sltval2  33158  sltintdifex  33163  fvsingle  33376  funpartfv  33401  fullfunfv  33403  rankeq1o  33627  atbase  36419  llnbase  36639  lplnbase  36664  lvolbase  36708  lhpbase  37128  mzpmfp  39337  kelac1  39656  mendbas  39777  mendplusgfval  39778  mendmulrfval  39780  mendsca  39782  mendvscafval  39783  brfvimex  40369  clsneibex  40445  neicvgbex  40455  sprssspr  43636  sprsymrelfvlem  43645  prprelprb  43672  prprspr2  43673  upwlkbprop  44006