Theorem fvprc 6874

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1567   ∈ wcel 2149  ∃!weu 2602  Vcvv 3463  ∅c0 4294   class class class wbr 5113  ‘cfv 6537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-nul 5271  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545

This theorem is referenced by:  rnfvprc  6876  dffv3  6878  fvrn0  6910  ndmfv  6914  fv2prc  6924  csbfv  6929  dffv2  6977  brfvopabrbr  6987  fvmpti  6989  fvmptnf  7013  fvmptrabfv  7023  fvunsn  7178  fvmptopab  7466  brfvopab  7468  1stval  7988  2ndval  7989  fipwuni  9386  fipwss  9389  tctr  9707  ranklim  9816  rankuni  9835  alephsing  10260  itunisuc  10403  itunitc  10405  tskmcl  10826  hashfn  14411  s1prc  14642  trclfvg  15052  trclfvcotrg  15053  dfrtrclrec2  15095  rtrclreclem4  15098  dfrtrcl2  15099  strfvss  17247  strfvi  17250  fveqprc  17251  oveqprc  17252  elbasfv  17275  ressbas  17296  firest  17485  topnval  17487  homffval  17746  comfffval  17754  oppchomfval  17770  xpcbas  18234  oduval  18344  oduleval  18345  lubfun  18406  glbfun  18419  odujoin  18462  odumeet  18464  oduclatb  18563  ipopos  18592  isipodrs  18593  plusffval  18704  grpidval  18719  gsum0  18742  ismnd  18795  frmdplusg  18913  frmd0  18919  efmndbas  18930  efmndbasabf  18931  efmndplusg  18939  dfgrp2e  19030  grpinvfval  19045  grpinvfvalALT  19046  grpinvfvi  19049  grpsubfval  19050  grpsubfvalALT  19051  mulgfval  19135  mulgfvalALT  19136  mulgfvi  19139  cntrval  19389  cntzval  19391  cntzrcl  19397  oppgval  19417  oppgplusfval  19418  symgval  19441  lactghmga  19475  psgnfval  19570  odfval  19602  odfvalALT  19603  oppglsm  19712  efgval  19787  mgpval  20219  mgpplusg  20220  ringidval  20265  opprval  20420  opprmulfval  20421  dvdsrval  20443  invrfval  20471  dvrfval  20484  rrgval  20782  staffval  20922  scaffval  20979  islss  21033  sralem  21275  sravsca  21280  sraip  21281  rlmval  21290  rlmsca2  21298  2idlval  21361  zrhval  21626  zlmvsca  21640  chrval  21642  evpmss  21705  ipffval  21767  ocvval  21786  elocv  21787  thlbas  21815  thlle  21816  thloc  21818  pjfval  21825  asclfval  21997  psrbas  22053  psr1val  22315  vr1val  22321  ply1val  22323  ply1basfvi  22369  ply1plusgfvi  22370  psr1sca2  22379  ply1sca2  22382  ply1ascl  22388  evl1fval  22457  evl1fval1  22460  toponsspwpw  23048  istps  23060  tgdif0  23118  indislem  23126  txindislem  23759  fsubbas  23993  filuni  24011  ussval  24385  isusp  24387  nmfval  24714  tngds  24774  tcphval  25346  deg1fval  26206  deg1fvi  26211  uc1pval  26266  mon1pval  26268  ltsval2  27786  ltsintdifex  27791  vtxval  29291  iedgval  29292  vtxvalprc  29336  iedgvalprc  29337  edgval  29340  prcliscplgr  29705  wwlks  30125  wwlksn  30127  clwwlk  30275  clwwlkn  30318  clwwlknonmpo  30381  vafval  30896  bafval  30897  smfval  30898  vsfval  30926  erlval  33519  fracval  33568  fracbas  33569  resvsca  33595  prclisacycgr  35542  mvtval  35891  mexval  35893  mexval2  35894  mdvval  35895  mrsubfval  35899  msubfval  35915  elmsubrn  35919  mvhfval  35924  mpstval  35926  msrfval  35928  mstaval  35935  mclsrcl  35952  mppsval  35963  mthmval  35966  fvsingle  36309  funpartfv  36336  fullfunfv  36338  rankeq1o  36562  atbase  39953  llnbase  40173  lplnbase  40198  lvolbase  40242  lhpbase  40662  mzpmfp  43370  kelac1  43682  mendbas  43799  mendplusgfval  43800  mendmulrfval  43802  mendvscafval  43805  brfvimex  44644  clsneibex  44720  neicvgbex  44730  sprssspr  48119  sprsymrelfvlem  48128  prprelprb  48155  prprspr2  48156  upwlkbprop  48792  ipolub00  49656  resccat  49737  oppcup3  49872  initopropdlem  49903  termopropdlem  49904  zeroopropdlem  49905  catcrcl  50058