Theorem fvprc 6826

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ∈ wcel 2113  ∃!weu 2568  Vcvv 3440  ∅c0 4285   class class class wbr 5098  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500

This theorem is referenced by:  rnfvprc  6828  dffv3  6830  fvrn0  6862  ndmfv  6866  fv2prc  6876  csbfv  6881  dffv2  6929  brfvopabrbr  6938  fvmpti  6940  fvmptnf  6963  fvmptrabfv  6973  fvunsn  7125  fvmptopab  7413  brfvopab  7415  1stval  7935  2ndval  7936  fipwuni  9329  fipwss  9332  tctr  9647  ranklim  9756  rankuni  9775  alephsing  10186  itunisuc  10329  itunitc  10331  tskmcl  10752  hashfn  14298  s1prc  14528  trclfvg  14938  trclfvcotrg  14939  dfrtrclrec2  14981  rtrclreclem4  14984  dfrtrcl2  14985  strfvss  17114  strfvi  17117  fveqprc  17118  oveqprc  17119  elbasfv  17142  ressbas  17163  firest  17352  topnval  17354  homffval  17613  comfffval  17621  oppchomfval  17637  xpcbas  18101  oduval  18211  oduleval  18212  lubfun  18273  glbfun  18286  odujoin  18329  odumeet  18331  oduclatb  18430  ipopos  18459  isipodrs  18460  plusffval  18571  grpidval  18586  gsum0  18609  ismnd  18662  frmdplusg  18779  frmd0  18785  efmndbas  18796  efmndbasabf  18797  efmndplusg  18805  dfgrp2e  18893  grpinvfval  18908  grpinvfvalALT  18909  grpinvfvi  18912  grpsubfval  18913  grpsubfvalALT  18914  mulgfval  18999  mulgfvalALT  19000  mulgfvi  19003  cntrval  19248  cntzval  19250  cntzrcl  19256  oppgval  19276  oppgplusfval  19277  symgval  19300  lactghmga  19334  psgnfval  19429  odfval  19461  odfvalALT  19462  oppglsm  19571  efgval  19646  mgpval  20078  mgpplusg  20079  ringidval  20118  opprval  20274  opprmulfval  20275  dvdsrval  20297  invrfval  20325  dvrfval  20338  rrgval  20630  staffval  20774  scaffval  20831  islss  20885  sralem  21128  sravsca  21133  sraip  21134  rlmval  21143  rlmsca2  21151  2idlval  21206  zrhval  21462  zlmvsca  21476  chrval  21478  evpmss  21541  ipffval  21603  ocvval  21622  elocv  21623  thlbas  21651  thlle  21652  thloc  21654  pjfval  21661  asclfval  21834  psrbas  21889  psr1val  22126  vr1val  22132  ply1val  22134  ply1basfvi  22181  ply1plusgfvi  22182  psr1sca2  22191  ply1sca2  22194  ply1ascl  22200  evl1fval  22272  evl1fval1  22275  toponsspwpw  22866  istps  22878  tgdif0  22936  indislem  22944  txindislem  23577  fsubbas  23811  filuni  23829  ussval  24203  isusp  24205  nmfval  24532  tngds  24592  tcphval  25174  deg1fval  26041  deg1fvi  26046  uc1pval  26101  mon1pval  26103  ltsval2  27624  ltsintdifex  27629  vtxval  29073  iedgval  29074  vtxvalprc  29118  iedgvalprc  29119  edgval  29122  prcliscplgr  29487  wwlks  29908  wwlksn  29910  clwwlk  30058  clwwlkn  30101  clwwlknonmpo  30164  vafval  30678  bafval  30679  smfval  30680  vsfval  30708  erlval  33340  fracval  33386  fracbas  33387  resvsca  33413  prclisacycgr  35345  mvtval  35694  mexval  35696  mexval2  35697  mdvval  35698  mrsubfval  35702  msubfval  35718  elmsubrn  35722  mvhfval  35727  mpstval  35729  msrfval  35731  mstaval  35738  mclsrcl  35755  mppsval  35766  mthmval  35769  fvsingle  36112  funpartfv  36139  fullfunfv  36141  rankeq1o  36365  atbase  39549  llnbase  39769  lplnbase  39794  lvolbase  39838  lhpbase  40258  mzpmfp  42989  kelac1  43305  mendbas  43422  mendplusgfval  43423  mendmulrfval  43425  mendvscafval  43428  brfvimex  44267  clsneibex  44343  neicvgbex  44353  sprssspr  47727  sprsymrelfvlem  47736  prprelprb  47763  prprspr2  47764  upwlkbprop  48384  ipolub00  49238  resccat  49319  oppcup3  49454  initopropdlem  49485  termopropdlem  49486  zeroopropdlem  49487  catcrcl  49640