Theorem fvprc 6097

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1475   ∈ wcel 1977  ∃!weu 2458  Vcvv 3173  ∅c0 3874   class class class wbr 4583  ‘cfv 5804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-nul 4717  ax-pow 4769

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812

This theorem is referenced by:  dffv3  6099  fvrn0  6126  ndmfv  6128  fv2prc  6138  csbfv  6143  dffv2  6181  fvmpti  6190  fvmptnf  6210  fvunsn  6350  brfvopab  6598  1stval  7061  2ndval  7062  fipwuni  8215  fipwss  8218  tctr  8499  ranklim  8590  rankuni  8609  alephsing  8981  itunisuc  9124  itunitc1  9125  itunitc  9126  tskmcl  9542  hashfn  13025  trclfvg  13604  trclfvcotrg  13605  strfvss  15713  strfvi  15741  setsnid  15743  elbasfv  15748  ressbas  15757  resslem  15760  firest  15916  topnval  15918  homffval  16173  comfffval  16181  oppchomfval  16197  oppcbas  16201  xpcbas  16641  lubfun  16803  glbfun  16816  oduval  16953  oduleval  16954  odumeet  16963  odujoin  16965  oduclatb  16967  ipopos  16983  isipodrs  16984  plusffval  17070  grpidval  17083  gsum0  17101  ismnd  17120  frmdplusg  17214  frmd0  17220  dfgrp2e  17271  grpinvfval  17283  grpinvfvi  17286  grpsubfval  17287  mulgfval  17365  mulgfvi  17368  cntrval  17575  cntzval  17577  cntzrcl  17583  oppgval  17600  oppgplusfval  17601  symgbas  17623  symgplusg  17632  lactghmga  17647  pmtrfrn  17701  psgnfval  17743  odfval  17775  oppglsm  17880  efgval  17953  mgpval  18315  mgpplusg  18316  ringidval  18326  opprval  18447  opprmulfval  18448  dvdsrval  18468  invrfval  18496  dvrfval  18507  staffval  18670  scaffval  18704  islss  18756  sralem  18998  srasca  19002  sravsca  19003  sraip  19004  rlmval  19012  rlmsca2  19022  2idlval  19054  rrgval  19108  asclfval  19155  psrbas  19199  psr1val  19377  vr1val  19383  ply1val  19385  ply1basfvi  19432  ply1plusgfvi  19433  psr1sca2  19442  ply1sca2  19445  ply1ascl  19449  evl1fval  19513  evl1fval1  19516  zrhval  19675  zlmlem  19684  zlmvsca  19689  chrval  19692  evpmss  19751  ipffval  19812  ocvval  19830  elocv  19831  thlbas  19859  thlle  19860  thloc  19862  pjfval  19869  istps  20551  tgdif0  20607  indislem  20614  txindislem  21246  fsubbas  21481  filuni  21499  ussval  21873  isusp  21875  nmfval  22203  tnglem  22254  tngds  22262  tchval  22825  deg1fval  23644  deg1fvi  23649  uc1pval  23703  mon1pval  23705  ttglem  25556  vtxvalprc  25720  iedgvalprc  25721  vafval  26842  bafval  26843  smfval  26844  vsfval  26872  resvsca  29161  resvlem  29162  mvtval  30651  mexval  30653  mexval2  30654  mdvval  30655  mrsubfval  30659  mrsubrn  30664  mrsub0  30667  mrsubf  30668  mrsubccat  30669  mrsubcn  30670  mrsubco  30672  mrsubvrs  30673  msubfval  30675  elmsubrn  30679  msubrn  30680  msubf  30683  mvhfval  30684  mpstval  30686  msrfval  30688  mstaval  30695  mclsrcl  30712  mppsval  30723  mthmval  30726  sltval2  31053  sltintdifex  31060  fvsingle  31197  funpartfv  31222  fullfunfv  31224  rankeq1o  31448  bj-toponss  32241  atbase  33594  llnbase  33813  lplnbase  33838  lvolbase  33882  lhpbase  34302  mzpmfp  36328  kelac1  36651  mendbas  36773  mendplusgfval  36774  mendmulrfval  36776  mendsca  36778  mendvscafval  36779  brfvimex  37344  clsneibex  37420  neicvgbex  37430  uvtxa0  40620  uvtxa01vtx  40624  wlkbProp  40817  wwlks  41038  wwlksn  41040  clwwlks  41187  clwwlksn  41189