Theorem fvprc 6878

Description: A function's value at a proper class is the empty set. See fvprcALT 6879 for a proof that uses ax-pow 5326 instead of ax-pr 5390. (Contributed by NM, 20-May-1998.) Avoid ax-pow 5326. (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 6876	. 2 ⊢ (¬ 𝐴 ∈ V → ¬ ∃!𝑥 𝐴𝐹𝑥)
2		tz6.12-2 6873	. 2 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅)
3	1, 2	syl 18	1 ⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1569   ∈ wcel 2144  ∃!weu 2593  Vcvv 3450  ∅c0 4278   class class class wbr 5102  ‘cfv 6539

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6547

This theorem is used by:  rnfvprc  6880  dffv3  6882  fvrn0  6914  ndmfv  6918  fv2prc  6928  csbfv  6933  dffv2  6981  brfvopabrbr  6991  fvmpti  6993  fvmptnf  7017  fvmptrabfv  7027  fvunsn  7185  fvmptopab  7476  brfvopab  7478  1stval  8004  2ndval  8005  fipwuni  9422  fipwss  9425  tctr  9743  ranklim  9862  rankuni  9883  alephsing  10358  itunisuc  10501  itunitc  10503  tskmcl  10930  hashfn  14523  s1prc  14755  trclfvg  15174  trclfvcotrg  15175  dfrtrclrec2  15217  rtrclreclem4  15220  dfrtrcl2  15221  strfvss  17371  strfvi  17374  fveqprc  17375  oveqprc  17376  elbasfv  17399  ressbas  17420  firest  17609  topnval  17611  homffval  17870  comfffval  17878  oppchomfval  17894  xpcbas  18358  oduval  18468  oduleval  18469  lubfun  18530  glbfun  18543  odujoin  18586  odumeet  18588  oduclatb  18687  ipopos  18716  isipodrs  18717  plusffval  18828  grpidval  18846  gsum0  18879  ismnd  18932  frmdplusg  19056  frmd0  19062  efmndbas  19073  efmndbasabf  19074  efmndplusg  19082  dfgrp2e  19180  grpinvfval  19195  grpinvfvalALT  19196  grpinvfvi  19199  grpsubfval  19200  grpsubfvalALT  19201  mulgfval  19285  mulgfvalALT  19286  mulgfvi  19289  cntrval  19539  cntzval  19541  cntzrcl  19547  oppgval  19567  oppgplusfval  19568  symgval  19591  lactghmga  19625  psgnfval  19720  odfval  19752  odfvalALT  19753  oppglsm  19862  efgval  19937  mgpval  20369  mgpplusg  20370  ringidval  20415  opprval  20574  opprmulfval  20575  dvdsrval  20597  invrfval  20625  dvrfval  20638  rrgval  20955  staffval  21104  scaffval  21161  islss  21215  sralem  21457  sravsca  21462  sraip  21463  rlmval  21472  rlmsca2  21480  2idlval  21550  zrhval  21819  zlmvsca  21833  chrval  21835  evpmss  21898  ipffval  21960  ocvval  21979  elocv  21980  thlbas  22008  thlle  22009  thloc  22011  pjfval  22018  asclfval  22192  psrbas  22248  psr1val  22510  vr1val  22516  ply1val  22518  ply1basfvi  22564  ply1plusgfvi  22565  psr1sca2  22574  ply1sca2  22577  ply1ascl  22583  evl1fval  22652  evl1fval1  22655  toponsspwpw  23246  istps  23258  tgdif0  23316  indislem  23324  txindislem  23958  fsubbas  24192  filuni  24210  ussval  24584  isusp  24586  nmfval  24913  tngds  24973  tcphval  25545  deg1fval  26404  deg1fvi  26409  uc1pval  26464  mon1pval  26466  ltsval2  28019  ltsintdifex  28024  vtxval  29584  iedgval  29585  vtxvalprc  29629  iedgvalprc  29630  edgval  29633  prcliscplgr  30001  wwlks  30430  wwlksn  30432  clwwlk  30580  clwwlkn  30623  clwwlknonmpo  30686  vafval  31211  bafval  31212  smfval  31213  vsfval  31241  erlval  33866  fracval  33913  fracbas  33914  resvsca  33940  kardval  35877  kardeq0  35881  kard0b  35884  kardcard2b  35890  prclisacycgr  35993  mvtval  36352  mexval  36354  mexval2  36355  mdvval  36356  mrsubfval  36360  msubfval  36376  elmsubrn  36380  mvhfval  36385  mpstval  36387  msrfval  36389  mstaval  36396  mclsrcl  36413  mppsval  36424  mthmval  36427  fvsingle  36775  funpartfv  36802  fullfunfv  36804  rankeq1o  37025  atbase  40440  llnbase  40660  lplnbase  40685  lvolbase  40729  lhpbase  41149  mzpmfp  43852  kelac1  44159  mendbas  44276  mendplusgfval  44277  mendmulrfval  44279  mendvscafval  44282  brfvimex  45120  clsneibex  45196  neicvgbex  45206  sprssspr  48657  sprsymrelfvlem  48666  prprelprb  48693  prprspr2  48694  upwlkbprop  49330  ipolub00  50201  resccat  50282  oppcup3  50419  initopropdlem  50456  termopropdlem  50457  zeroopropdlem  50458  catcrcl  50624