Theorem fvprc 6183

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1482   ∈ wcel 1989  ∃!weu 2469  Vcvv 3198  ∅c0 3913   class class class wbr 4651  ‘cfv 5886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-8 1991  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-nul 4787  ax-pow 4841

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ral 2916  df-rex 2917  df-rab 2920  df-v 3200  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-nul 3914  df-if 4085  df-sn 4176  df-pr 4178  df-op 4182  df-uni 4435  df-br 4652  df-iota 5849  df-fv 5894

This theorem is referenced by:  dffv3  6185  fvrn0  6214  ndmfv  6216  fv2prc  6226  csbfv  6231  dffv2  6269  brfvopabrbr  6277  fvmpti  6279  fvmptnf  6300  fvunsn  6442  fvmptopab  6694  brfvopab  6697  1stval  7167  2ndval  7168  fipwuni  8329  fipwss  8332  tctr  8613  ranklim  8704  rankuni  8723  alephsing  9095  itunisuc  9238  itunitc1  9239  itunitc  9240  tskmcl  9660  hashfn  13159  trclfvg  13750  trclfvcotrg  13751  strfvss  15874  strfvi  15907  setsnid  15909  elbasfv  15914  ressbas  15924  resslem  15927  firest  16087  topnval  16089  homffval  16344  comfffval  16352  oppchomfval  16368  oppcbas  16372  xpcbas  16812  lubfun  16974  glbfun  16987  oduval  17124  oduleval  17125  odumeet  17134  odujoin  17136  oduclatb  17138  ipopos  17154  isipodrs  17155  plusffval  17241  grpidval  17254  gsum0  17272  ismnd  17291  frmdplusg  17385  frmd0  17391  dfgrp2e  17442  grpinvfval  17454  grpinvfvi  17457  grpsubfval  17458  mulgfval  17536  mulgfvi  17539  cntrval  17746  cntzval  17748  cntzrcl  17754  oppgval  17771  oppgplusfval  17772  symgbas  17794  symgplusg  17803  lactghmga  17818  pmtrfrn  17872  psgnfval  17914  odfval  17946  oppglsm  18051  efgval  18124  mgpval  18486  mgpplusg  18487  ringidval  18497  opprval  18618  opprmulfval  18619  dvdsrval  18639  invrfval  18667  dvrfval  18678  staffval  18841  scaffval  18875  islss  18929  sralem  19171  srasca  19175  sravsca  19176  sraip  19177  rlmval  19185  rlmsca2  19195  2idlval  19227  rrgval  19281  asclfval  19328  psrbas  19372  psr1val  19550  vr1val  19556  ply1val  19558  ply1basfvi  19605  ply1plusgfvi  19606  psr1sca2  19615  ply1sca2  19618  ply1ascl  19622  evl1fval  19686  evl1fval1  19689  zrhval  19850  zlmlem  19859  zlmvsca  19864  chrval  19867  evpmss  19926  ipffval  19987  ocvval  20005  elocv  20006  thlbas  20034  thlle  20035  thloc  20037  pjfval  20044  toponsspwpw  20720  istps  20732  tgdif0  20790  indislem  20798  txindislem  21430  fsubbas  21665  filuni  21683  ussval  22057  isusp  22059  nmfval  22387  tnglem  22438  tngds  22446  tchval  23011  deg1fval  23834  deg1fvi  23839  uc1pval  23893  mon1pval  23895  ttglem  25750  vtxval  25872  iedgval  25873  vtxvalprc  25931  iedgvalprc  25932  edgval  25935  uvtxa0  26288  uvtxa01vtx  26292  wwlks  26721  wwlksn  26723  clwwlks  26873  clwwlksn  26875  vafval  27442  bafval  27443  smfval  27444  vsfval  27472  resvsca  29815  resvlem  29816  mvtval  31382  mexval  31384  mexval2  31385  mdvval  31386  mrsubfval  31390  mrsubrn  31395  mrsub0  31398  mrsubf  31399  mrsubccat  31400  mrsubcn  31401  mrsubco  31403  mrsubvrs  31404  msubfval  31406  elmsubrn  31410  msubrn  31411  msubf  31414  mvhfval  31415  mpstval  31417  msrfval  31419  mstaval  31426  mclsrcl  31443  mppsval  31454  mthmval  31457  sltval2  31793  sltintdifex  31798  fvsingle  32011  funpartfv  32036  fullfunfv  32038  rankeq1o  32262  atbase  34402  llnbase  34621  lplnbase  34646  lvolbase  34690  lhpbase  35110  mzpmfp  37136  kelac1  37459  mendbas  37580  mendplusgfval  37581  mendmulrfval  37583  mendsca  37585  mendvscafval  37586  brfvimex  38150  clsneibex  38226  neicvgbex  38236  upwlkbprop  41490  sprssspr  41502  sprsymrelfvlem  41511