Theorem fvprc 6834

Description: A function's value at a proper class is the empty set. See fvprcALT 6835 for a proof that uses ax-pow 5312 instead of ax-pr 5379. (Contributed by NM, 20-May-1998.) Avoid ax-pow 5312. (Revised by BTernaryTau, 3-Aug-2024.) (Proof shortened by BTernaryTau, 3-Dec-2024.)

Assertion

Ref	Expression
fvprc	⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅)

Proof of Theorem fvprc

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		brprcneu 6832	. 2 ⊢ (¬ 𝐴 ∈ V → ¬ ∃!𝑥 𝐴𝐹𝑥)
2		tz6.12-2 6829	. 2 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅)
3	1, 2	syl 17	1 ⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ∈ wcel 2114  ∃!weu 2569  Vcvv 3442  ∅c0 4287   class class class wbr 5100  ‘cfv 6500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508

This theorem is referenced by:  rnfvprc  6836  dffv3  6838  fvrn0  6870  ndmfv  6874  fv2prc  6884  csbfv  6889  dffv2  6937  brfvopabrbr  6946  fvmpti  6948  fvmptnf  6972  fvmptrabfv  6982  fvunsn  7135  fvmptopab  7423  brfvopab  7425  1stval  7945  2ndval  7946  fipwuni  9341  fipwss  9344  tctr  9659  ranklim  9768  rankuni  9787  alephsing  10198  itunisuc  10341  itunitc  10343  tskmcl  10764  hashfn  14310  s1prc  14540  trclfvg  14950  trclfvcotrg  14951  dfrtrclrec2  14993  rtrclreclem4  14996  dfrtrcl2  14997  strfvss  17126  strfvi  17129  fveqprc  17130  oveqprc  17131  elbasfv  17154  ressbas  17175  firest  17364  topnval  17366  homffval  17625  comfffval  17633  oppchomfval  17649  xpcbas  18113  oduval  18223  oduleval  18224  lubfun  18285  glbfun  18298  odujoin  18341  odumeet  18343  oduclatb  18442  ipopos  18471  isipodrs  18472  plusffval  18583  grpidval  18598  gsum0  18621  ismnd  18674  frmdplusg  18791  frmd0  18797  efmndbas  18808  efmndbasabf  18809  efmndplusg  18817  dfgrp2e  18905  grpinvfval  18920  grpinvfvalALT  18921  grpinvfvi  18924  grpsubfval  18925  grpsubfvalALT  18926  mulgfval  19011  mulgfvalALT  19012  mulgfvi  19015  cntrval  19260  cntzval  19262  cntzrcl  19268  oppgval  19288  oppgplusfval  19289  symgval  19312  lactghmga  19346  psgnfval  19441  odfval  19473  odfvalALT  19474  oppglsm  19583  efgval  19658  mgpval  20090  mgpplusg  20091  ringidval  20130  opprval  20286  opprmulfval  20287  dvdsrval  20309  invrfval  20337  dvrfval  20350  rrgval  20642  staffval  20786  scaffval  20843  islss  20897  sralem  21140  sravsca  21145  sraip  21146  rlmval  21155  rlmsca2  21163  2idlval  21218  zrhval  21474  zlmvsca  21488  chrval  21490  evpmss  21553  ipffval  21615  ocvval  21634  elocv  21635  thlbas  21663  thlle  21664  thloc  21666  pjfval  21673  asclfval  21846  psrbas  21901  psr1val  22138  vr1val  22144  ply1val  22146  ply1basfvi  22193  ply1plusgfvi  22194  psr1sca2  22203  ply1sca2  22206  ply1ascl  22212  evl1fval  22284  evl1fval1  22287  toponsspwpw  22878  istps  22890  tgdif0  22948  indislem  22956  txindislem  23589  fsubbas  23823  filuni  23841  ussval  24215  isusp  24217  nmfval  24544  tngds  24604  tcphval  25186  deg1fval  26053  deg1fvi  26058  uc1pval  26113  mon1pval  26115  ltsval2  27636  ltsintdifex  27641  vtxval  29085  iedgval  29086  vtxvalprc  29130  iedgvalprc  29131  edgval  29134  prcliscplgr  29499  wwlks  29920  wwlksn  29922  clwwlk  30070  clwwlkn  30113  clwwlknonmpo  30176  vafval  30691  bafval  30692  smfval  30693  vsfval  30721  erlval  33352  fracval  33398  fracbas  33399  resvsca  33425  prclisacycgr  35367  mvtval  35716  mexval  35718  mexval2  35719  mdvval  35720  mrsubfval  35724  msubfval  35740  elmsubrn  35744  mvhfval  35749  mpstval  35751  msrfval  35753  mstaval  35760  mclsrcl  35777  mppsval  35788  mthmval  35791  fvsingle  36134  funpartfv  36161  fullfunfv  36163  rankeq1o  36387  atbase  39665  llnbase  39885  lplnbase  39910  lvolbase  39954  lhpbase  40374  mzpmfp  43104  kelac1  43420  mendbas  43537  mendplusgfval  43538  mendmulrfval  43540  mendvscafval  43543  brfvimex  44382  clsneibex  44458  neicvgbex  44468  sprssspr  47841  sprsymrelfvlem  47850  prprelprb  47877  prprspr2  47878  upwlkbprop  48498  ipolub00  49352  resccat  49433  oppcup3  49568  initopropdlem  49599  termopropdlem  49600  zeroopropdlem  49601  catcrcl  49754