Theorem fvprc 6898

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1536   ∈ wcel 2105  ∃!weu 2565  Vcvv 3477  ∅c0 4338   class class class wbr 5147  ‘cfv 6562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570

This theorem is referenced by:  rnfvprc  6900  dffv3  6902  fvrn0  6936  ndmfv  6941  fv2prc  6951  csbfv  6956  dffv2  7003  brfvopabrbr  7012  fvmpti  7014  fvmptnf  7037  fvmptrabfv  7047  fvunsn  7198  fvmptopab  7486  fvmptopabOLD  7487  brfvopab  7489  1stval  8014  2ndval  8015  fipwuni  9463  fipwss  9466  tctr  9777  ranklim  9881  rankuni  9900  alephsing  10313  itunisuc  10456  itunitc  10458  tskmcl  10878  hashfn  14410  s1prc  14638  trclfvg  15050  trclfvcotrg  15051  dfrtrclrec2  15093  rtrclreclem4  15096  dfrtrcl2  15097  strfvss  17220  strfvi  17223  fveqprc  17224  oveqprc  17225  setsnidOLD  17243  elbasfv  17250  ressbas  17279  ressbasOLD  17280  resslemOLD  17287  firest  17478  topnval  17480  homffval  17734  comfffval  17742  oppchomfval  17758  oppchomfvalOLD  17759  oppcbasOLD  17764  xpcbas  18233  oduval  18344  oduleval  18345  lubfun  18409  glbfun  18422  odujoin  18465  odumeet  18467  oduclatb  18564  ipopos  18593  isipodrs  18594  plusffval  18671  grpidval  18686  gsum0  18709  ismnd  18762  frmdplusg  18879  frmd0  18885  efmndbas  18896  efmndbasabf  18897  efmndplusg  18905  dfgrp2e  18993  grpinvfval  19008  grpinvfvalALT  19009  grpinvfvi  19012  grpsubfval  19013  grpsubfvalALT  19014  mulgfval  19099  mulgfvalALT  19100  mulgfvi  19103  cntrval  19349  cntzval  19351  cntzrcl  19357  oppgval  19377  oppgplusfval  19378  symgval  19402  lactghmga  19437  psgnfval  19532  odfval  19564  odfvalALT  19565  oppglsm  19674  efgval  19749  mgpval  20154  mgpplusg  20155  ringidval  20200  opprval  20351  opprmulfval  20352  dvdsrval  20377  invrfval  20405  dvrfval  20418  rrgval  20713  staffval  20858  scaffval  20894  islss  20949  sralem  21192  sralemOLD  21193  sravsca  21202  sravscaOLD  21203  sraip  21204  rlmval  21215  rlmsca2  21223  2idlval  21278  zrhval  21535  zlmlemOLD  21545  zlmvsca  21553  chrval  21555  evpmss  21621  ipffval  21683  ocvval  21702  elocv  21703  thlbas  21731  thlbasOLD  21732  thlle  21733  thlleOLD  21734  thloc  21736  pjfval  21743  asclfval  21916  psrbas  21970  psr1val  22202  vr1val  22208  ply1val  22210  ply1basfvi  22257  ply1plusgfvi  22258  psr1sca2  22267  ply1sca2  22270  ply1ascl  22276  evl1fval  22347  evl1fval1  22350  toponsspwpw  22943  istps  22955  tgdif0  23014  indislem  23022  txindislem  23656  fsubbas  23890  filuni  23908  ussval  24283  isusp  24285  nmfval  24616  tnglemOLD  24669  tngds  24683  tngdsOLD  24684  tcphval  25265  deg1fval  26133  deg1fvi  26138  uc1pval  26193  mon1pval  26195  sltval2  27715  sltintdifex  27720  ttglemOLD  28900  vtxval  29031  iedgval  29032  vtxvalprc  29076  iedgvalprc  29077  edgval  29080  prcliscplgr  29445  wwlks  29864  wwlksn  29866  clwwlk  30011  clwwlkn  30054  clwwlknonmpo  30117  vafval  30631  bafval  30632  smfval  30633  vsfval  30661  erlval  33244  fracval  33285  fracbas  33286  resvsca  33335  resvlemOLD  33337  prclisacycgr  35135  mvtval  35484  mexval  35486  mexval2  35487  mdvval  35488  mrsubfval  35492  msubfval  35508  elmsubrn  35512  mvhfval  35517  mpstval  35519  msrfval  35521  mstaval  35528  mclsrcl  35545  mppsval  35556  mthmval  35559  fvsingle  35901  funpartfv  35926  fullfunfv  35928  rankeq1o  36152  atbase  39270  llnbase  39491  lplnbase  39516  lvolbase  39560  lhpbase  39980  mzpmfp  42734  kelac1  43051  mendbas  43168  mendplusgfval  43169  mendmulrfval  43171  mendvscafval  43174  brfvimex  44015  clsneibex  44091  neicvgbex  44101  sprssspr  47405  sprsymrelfvlem  47414  prprelprb  47441  prprspr2  47442  upwlkbprop  47981  ipolub00  48781