Theorem fvprc 6819

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1547   ∈ wcel 2119  ∃!weu 2572  Vcvv 3431  ∅c0 4261   class class class wbr 5072  ‘cfv 6485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-nul 5228  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-iota 6441  df-fv 6493

This theorem is referenced by:  rnfvprc  6821  dffv3  6823  fvrn0  6855  ndmfv  6859  fv2prc  6869  csbfv  6874  dffv2  6922  brfvopabrbr  6932  fvmpti  6934  fvmptnf  6958  fvmptrabfv  6968  fvunsn  7123  fvmptopab  7411  brfvopab  7413  1stval  7933  2ndval  7934  fipwuni  9329  fipwss  9332  tctr  9650  ranklim  9759  rankuni  9778  alephsing  10189  itunisuc  10332  itunitc  10334  tskmcl  10755  hashfn  14328  s1prc  14558  trclfvg  14968  trclfvcotrg  14969  dfrtrclrec2  15011  rtrclreclem4  15014  dfrtrcl2  15015  strfvss  17148  strfvi  17151  fveqprc  17152  oveqprc  17153  elbasfv  17176  ressbas  17197  firest  17386  topnval  17388  homffval  17647  comfffval  17655  oppchomfval  17671  xpcbas  18135  oduval  18245  oduleval  18246  lubfun  18307  glbfun  18320  odujoin  18363  odumeet  18365  oduclatb  18464  ipopos  18493  isipodrs  18494  plusffval  18605  grpidval  18620  gsum0  18643  ismnd  18696  frmdplusg  18813  frmd0  18819  efmndbas  18830  efmndbasabf  18831  efmndplusg  18839  dfgrp2e  18930  grpinvfval  18945  grpinvfvalALT  18946  grpinvfvi  18949  grpsubfval  18950  grpsubfvalALT  18951  mulgfval  19036  mulgfvalALT  19037  mulgfvi  19040  cntrval  19285  cntzval  19287  cntzrcl  19293  oppgval  19313  oppgplusfval  19314  symgval  19337  lactghmga  19371  psgnfval  19466  odfval  19498  odfvalALT  19499  oppglsm  19608  efgval  19683  mgpval  20115  mgpplusg  20116  ringidval  20155  opprval  20309  opprmulfval  20310  dvdsrval  20332  invrfval  20360  dvrfval  20373  rrgval  20669  staffval  20813  scaffval  20870  islss  20924  sralem  21166  sravsca  21171  sraip  21172  rlmval  21181  rlmsca2  21189  2idlval  21244  zrhval  21482  zlmvsca  21496  chrval  21498  evpmss  21561  ipffval  21623  ocvval  21642  elocv  21643  thlbas  21671  thlle  21672  thloc  21674  pjfval  21681  asclfval  21853  psrbas  21909  psr1val  22171  vr1val  22177  ply1val  22179  ply1basfvi  22225  ply1plusgfvi  22226  psr1sca2  22235  ply1sca2  22238  ply1ascl  22244  evl1fval  22314  evl1fval1  22317  toponsspwpw  22905  istps  22917  tgdif0  22975  indislem  22983  txindislem  23616  fsubbas  23850  filuni  23868  ussval  24242  isusp  24244  nmfval  24571  tngds  24631  tcphval  25203  deg1fval  26063  deg1fvi  26068  uc1pval  26123  mon1pval  26125  ltsval2  27638  ltsintdifex  27643  vtxval  29087  iedgval  29088  vtxvalprc  29132  iedgvalprc  29133  edgval  29136  prcliscplgr  29501  wwlks  29921  wwlksn  29923  clwwlk  30071  clwwlkn  30114  clwwlknonmpo  30177  vafval  30692  bafval  30693  smfval  30694  vsfval  30722  erlval  33339  fracval  33388  fracbas  33389  resvsca  33415  prclisacycgr  35379  mvtval  35728  mexval  35730  mexval2  35731  mdvval  35732  mrsubfval  35736  msubfval  35752  elmsubrn  35756  mvhfval  35761  mpstval  35763  msrfval  35765  mstaval  35772  mclsrcl  35789  mppsval  35800  mthmval  35803  fvsingle  36146  funpartfv  36173  fullfunfv  36175  rankeq1o  36399  atbase  39781  llnbase  40001  lplnbase  40026  lvolbase  40070  lhpbase  40490  mzpmfp  43196  kelac1  43508  mendbas  43625  mendplusgfval  43626  mendmulrfval  43628  mendvscafval  43631  brfvimex  44470  clsneibex  44546  neicvgbex  44556  sprssspr  47956  sprsymrelfvlem  47965  prprelprb  47992  prprspr2  47993  upwlkbprop  48629  ipolub00  49483  resccat  49564  oppcup3  49699  initopropdlem  49730  termopropdlem  49731  zeroopropdlem  49732  catcrcl  49885