Theorem fvprc 6883

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ∈ wcel 2106  ∃!weu 2562  Vcvv 3474  ∅c0 4322   class class class wbr 5148  ‘cfv 6543

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551

This theorem is referenced by:  rnfvprc  6885  dffv3  6887  fvrn0  6921  ndmfv  6926  fv2prc  6936  csbfv  6941  dffv2  6986  brfvopabrbr  6995  fvmpti  6997  fvmptnf  7020  fvmptrabfv  7029  fvunsn  7179  fvmptopab  7465  fvmptopabOLD  7466  brfvopab  7468  1stval  7979  2ndval  7980  fipwuni  9423  fipwss  9426  tctr  9737  ranklim  9841  rankuni  9860  alephsing  10273  itunisuc  10416  itunitc  10418  tskmcl  10838  hashfn  14339  s1prc  14558  trclfvg  14966  trclfvcotrg  14967  dfrtrclrec2  15009  rtrclreclem4  15012  dfrtrcl2  15013  strfvss  17124  strfvi  17127  fveqprc  17128  oveqprc  17129  setsnidOLD  17147  elbasfv  17154  ressbas  17183  ressbasOLD  17184  resslemOLD  17191  firest  17382  topnval  17384  homffval  17638  comfffval  17646  oppchomfval  17662  oppchomfvalOLD  17663  oppcbasOLD  17668  xpcbas  18134  oduval  18245  oduleval  18246  lubfun  18309  glbfun  18322  odujoin  18365  odumeet  18367  oduclatb  18464  ipopos  18493  isipodrs  18494  plusffval  18571  grpidval  18586  gsum0  18609  ismnd  18662  frmdplusg  18771  frmd0  18777  efmndbas  18788  efmndbasabf  18789  efmndplusg  18797  dfgrp2e  18884  grpinvfval  18899  grpinvfvalALT  18900  grpinvfvi  18903  grpsubfval  18904  grpsubfvalALT  18905  mulgfval  18988  mulgfvalALT  18989  mulgfvi  18992  cntrval  19224  cntzval  19226  cntzrcl  19232  oppgval  19252  oppgplusfval  19253  symgval  19277  lactghmga  19314  psgnfval  19409  odfval  19441  odfvalALT  19442  oppglsm  19551  efgval  19626  mgpval  20031  mgpplusg  20032  ringidval  20077  opprval  20226  opprmulfval  20227  dvdsrval  20252  invrfval  20280  dvrfval  20293  staffval  20598  scaffval  20634  islss  20689  sralem  20935  sralemOLD  20936  sravsca  20945  sravscaOLD  20946  sraip  20947  rlmval  20958  rlmsca2  20968  2idlval  21007  rrgval  21103  zrhval  21276  zlmlemOLD  21286  zlmvsca  21294  chrval  21296  evpmss  21358  ipffval  21420  ocvval  21439  elocv  21440  thlbas  21468  thlbasOLD  21469  thlle  21470  thlleOLD  21471  thloc  21473  pjfval  21480  asclfval  21652  psrbas  21716  psr1val  21929  vr1val  21935  ply1val  21937  ply1basfvi  21983  ply1plusgfvi  21984  psr1sca2  21993  ply1sca2  21996  ply1ascl  22000  evl1fval  22067  evl1fval1  22070  toponsspwpw  22644  istps  22656  tgdif0  22715  indislem  22723  txindislem  23357  fsubbas  23591  filuni  23609  ussval  23984  isusp  23986  nmfval  24317  tnglemOLD  24370  tngds  24384  tngdsOLD  24385  tcphval  24959  deg1fval  25822  deg1fvi  25827  uc1pval  25881  mon1pval  25883  sltval2  27383  sltintdifex  27388  ttglemOLD  28384  vtxval  28515  iedgval  28516  vtxvalprc  28560  iedgvalprc  28561  edgval  28564  prcliscplgr  28926  wwlks  29344  wwlksn  29346  clwwlk  29491  clwwlkn  29534  clwwlknonmpo  29597  vafval  30111  bafval  30112  smfval  30113  vsfval  30141  resvsca  32702  resvlemOLD  32704  prclisacycgr  34428  mvtval  34777  mexval  34779  mexval2  34780  mdvval  34781  mrsubfval  34785  msubfval  34801  elmsubrn  34805  mvhfval  34810  mpstval  34812  msrfval  34814  mstaval  34821  mclsrcl  34838  mppsval  34849  mthmval  34852  fvsingle  35184  funpartfv  35209  fullfunfv  35211  rankeq1o  35435  atbase  38462  llnbase  38683  lplnbase  38708  lvolbase  38752  lhpbase  39172  mzpmfp  41787  kelac1  42107  mendbas  42228  mendplusgfval  42229  mendmulrfval  42231  mendvscafval  42234  brfvimex  43079  clsneibex  43155  neicvgbex  43165  sprssspr  46448  sprsymrelfvlem  46457  prprelprb  46484  prprspr2  46485  upwlkbprop  46815  ipolub00  47706