Theorem fvprc 6832

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ∈ wcel 2114  ∃!weu 2568  Vcvv 3429  ∅c0 4273   class class class wbr 5085  ‘cfv 6498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-nul 5241  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506

This theorem is referenced by:  rnfvprc  6834  dffv3  6836  fvrn0  6868  ndmfv  6872  fv2prc  6882  csbfv  6887  dffv2  6935  brfvopabrbr  6944  fvmpti  6946  fvmptnf  6970  fvmptrabfv  6980  fvunsn  7134  fvmptopab  7422  brfvopab  7424  1stval  7944  2ndval  7945  fipwuni  9339  fipwss  9342  tctr  9659  ranklim  9768  rankuni  9787  alephsing  10198  itunisuc  10341  itunitc  10343  tskmcl  10764  hashfn  14337  s1prc  14567  trclfvg  14977  trclfvcotrg  14978  dfrtrclrec2  15020  rtrclreclem4  15023  dfrtrcl2  15024  strfvss  17157  strfvi  17160  fveqprc  17161  oveqprc  17162  elbasfv  17185  ressbas  17206  firest  17395  topnval  17397  homffval  17656  comfffval  17664  oppchomfval  17680  xpcbas  18144  oduval  18254  oduleval  18255  lubfun  18316  glbfun  18329  odujoin  18372  odumeet  18374  oduclatb  18473  ipopos  18502  isipodrs  18503  plusffval  18614  grpidval  18629  gsum0  18652  ismnd  18705  frmdplusg  18822  frmd0  18828  efmndbas  18839  efmndbasabf  18840  efmndplusg  18848  dfgrp2e  18939  grpinvfval  18954  grpinvfvalALT  18955  grpinvfvi  18958  grpsubfval  18959  grpsubfvalALT  18960  mulgfval  19045  mulgfvalALT  19046  mulgfvi  19049  cntrval  19294  cntzval  19296  cntzrcl  19302  oppgval  19322  oppgplusfval  19323  symgval  19346  lactghmga  19380  psgnfval  19475  odfval  19507  odfvalALT  19508  oppglsm  19617  efgval  19692  mgpval  20124  mgpplusg  20125  ringidval  20164  opprval  20318  opprmulfval  20319  dvdsrval  20341  invrfval  20369  dvrfval  20382  rrgval  20674  staffval  20818  scaffval  20875  islss  20929  sralem  21171  sravsca  21176  sraip  21177  rlmval  21186  rlmsca2  21194  2idlval  21249  zrhval  21487  zlmvsca  21501  chrval  21503  evpmss  21566  ipffval  21628  ocvval  21647  elocv  21648  thlbas  21676  thlle  21677  thloc  21679  pjfval  21686  asclfval  21858  psrbas  21913  psr1val  22149  vr1val  22155  ply1val  22157  ply1basfvi  22204  ply1plusgfvi  22205  psr1sca2  22214  ply1sca2  22217  ply1ascl  22223  evl1fval  22293  evl1fval1  22296  toponsspwpw  22887  istps  22899  tgdif0  22957  indislem  22965  txindislem  23598  fsubbas  23832  filuni  23850  ussval  24224  isusp  24226  nmfval  24553  tngds  24613  tcphval  25185  deg1fval  26045  deg1fvi  26050  uc1pval  26105  mon1pval  26107  ltsval2  27620  ltsintdifex  27625  vtxval  29069  iedgval  29070  vtxvalprc  29114  iedgvalprc  29115  edgval  29118  prcliscplgr  29483  wwlks  29903  wwlksn  29905  clwwlk  30053  clwwlkn  30096  clwwlknonmpo  30159  vafval  30674  bafval  30675  smfval  30676  vsfval  30704  erlval  33319  fracval  33365  fracbas  33366  resvsca  33392  prclisacycgr  35333  mvtval  35682  mexval  35684  mexval2  35685  mdvval  35686  mrsubfval  35690  msubfval  35706  elmsubrn  35710  mvhfval  35715  mpstval  35717  msrfval  35719  mstaval  35726  mclsrcl  35743  mppsval  35754  mthmval  35757  fvsingle  36100  funpartfv  36127  fullfunfv  36129  rankeq1o  36353  atbase  39735  llnbase  39955  lplnbase  39980  lvolbase  40024  lhpbase  40444  mzpmfp  43179  kelac1  43491  mendbas  43608  mendplusgfval  43609  mendmulrfval  43611  mendvscafval  43614  brfvimex  44453  clsneibex  44529  neicvgbex  44539  sprssspr  47941  sprsymrelfvlem  47950  prprelprb  47977  prprspr2  47978  upwlkbprop  48614  ipolub00  49468  resccat  49549  oppcup3  49684  initopropdlem  49715  termopropdlem  49716  zeroopropdlem  49717  catcrcl  49870