Theorem fvprc 6870

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ∈ wcel 2145  ∃!weu 2593  Vcvv 3450  ∅c0 4279   class class class wbr 5103  ‘cfv 6533

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-nul 5263  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  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-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541

This theorem is used by:  rnfvprc  6872  dffv3  6874  fvrn0  6906  ndmfv  6910  fv2prc  6920  csbfv  6925  dffv2  6973  brfvopabrbr  6983  fvmpti  6985  fvmptnf  7009  fvmptrabfv  7019  fvunsn  7177  fvmptopab  7468  brfvopab  7470  1stval  7988  2ndval  7989  fipwuni  9396  fipwss  9399  tctr  9717  ranklim  9826  rankuni  9845  alephsing  10278  itunisuc  10421  itunitc  10423  tskmcl  10850  hashfn  14439  s1prc  14671  trclfvg  15088  trclfvcotrg  15089  dfrtrclrec2  15131  rtrclreclem4  15134  dfrtrcl2  15135  strfvss  17279  strfvi  17282  fveqprc  17283  oveqprc  17284  elbasfv  17307  ressbas  17328  firest  17517  topnval  17519  homffval  17778  comfffval  17786  oppchomfval  17802  xpcbas  18266  oduval  18376  oduleval  18377  lubfun  18438  glbfun  18451  odujoin  18494  odumeet  18496  oduclatb  18595  ipopos  18624  isipodrs  18625  plusffval  18736  grpidval  18754  gsum0  18786  ismnd  18839  frmdplusg  18963  frmd0  18969  efmndbas  18980  efmndbasabf  18981  efmndplusg  18989  dfgrp2e  19087  grpinvfval  19102  grpinvfvalALT  19103  grpinvfvi  19106  grpsubfval  19107  grpsubfvalALT  19108  mulgfval  19192  mulgfvalALT  19193  mulgfvi  19196  cntrval  19446  cntzval  19448  cntzrcl  19454  oppgval  19474  oppgplusfval  19475  symgval  19498  lactghmga  19532  psgnfval  19627  odfval  19659  odfvalALT  19660  oppglsm  19769  efgval  19844  mgpval  20276  mgpplusg  20277  ringidval  20322  opprval  20479  opprmulfval  20480  dvdsrval  20502  invrfval  20530  dvrfval  20543  rrgval  20859  staffval  21007  scaffval  21064  islss  21118  sralem  21360  sravsca  21365  sraip  21366  rlmval  21375  rlmsca2  21383  2idlval  21453  zrhval  21720  zlmvsca  21734  chrval  21736  evpmss  21799  ipffval  21861  ocvval  21880  elocv  21881  thlbas  21909  thlle  21910  thloc  21912  pjfval  21919  asclfval  22093  psrbas  22149  psr1val  22411  vr1val  22417  ply1val  22419  ply1basfvi  22465  ply1plusgfvi  22466  psr1sca2  22475  ply1sca2  22478  ply1ascl  22484  evl1fval  22553  evl1fval1  22556  toponsspwpw  23147  istps  23159  tgdif0  23217  indislem  23225  txindislem  23859  fsubbas  24093  filuni  24111  ussval  24485  isusp  24487  nmfval  24814  tngds  24874  tcphval  25446  deg1fval  26305  deg1fvi  26310  uc1pval  26365  mon1pval  26367  ltsval2  27892  ltsintdifex  27897  vtxval  29457  iedgval  29458  vtxvalprc  29502  iedgvalprc  29503  edgval  29506  prcliscplgr  29874  wwlks  30303  wwlksn  30305  clwwlk  30453  clwwlkn  30496  clwwlknonmpo  30559  vafval  31084  bafval  31085  smfval  31086  vsfval  31114  erlval  33698  fracval  33745  fracbas  33746  resvsca  33772  kardval  35678  kardeq0  35682  kard0b  35685  kardcard2b  35691  prclisacycgr  35730  mvtval  36079  mexval  36081  mexval2  36082  mdvval  36083  mrsubfval  36087  msubfval  36103  elmsubrn  36107  mvhfval  36112  mpstval  36114  msrfval  36116  mstaval  36123  mclsrcl  36140  mppsval  36151  mthmval  36154  fvsingle  36497  funpartfv  36524  fullfunfv  36526  rankeq1o  36751  atbase  40162  llnbase  40382  lplnbase  40407  lvolbase  40451  lhpbase  40871  mzpmfp  43592  kelac1  43904  mendbas  44021  mendplusgfval  44022  mendmulrfval  44024  mendvscafval  44027  brfvimex  44866  clsneibex  44942  neicvgbex  44952  sprssspr  48381  sprsymrelfvlem  48390  prprelprb  48417  prprspr2  48418  upwlkbprop  49054  ipolub00  49919  resccat  50000  oppcup3  50135  initopropdlem  50166  termopropdlem  50167  zeroopropdlem  50168  catcrcl  50321