Theorem fvprc 6877

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ∈ wcel 2146  ∃!weu 2598  Vcvv 3457  ∅c0 4286   class class class wbr 5111  ‘cfv 6540

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 2148  ax-9 2156  ax-ext 2737  ax-nul 5271  ax-pr 5406

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548

This theorem is used by:  rnfvprc  6879  dffv3  6881  fvrn0  6913  ndmfv  6917  fv2prc  6927  csbfv  6932  dffv2  6980  brfvopabrbr  6990  fvmpti  6992  fvmptnf  7016  fvmptrabfv  7026  fvunsn  7181  fvmptopab  7471  brfvopab  7473  1stval  7990  2ndval  7991  fipwuni  9389  fipwss  9392  tctr  9710  ranklim  9819  rankuni  9838  alephsing  10271  itunisuc  10414  itunitc  10416  tskmcl  10837  hashfn  14425  s1prc  14657  trclfvg  15072  trclfvcotrg  15073  dfrtrclrec2  15115  rtrclreclem4  15118  dfrtrcl2  15119  strfvss  17265  strfvi  17268  fveqprc  17269  oveqprc  17270  elbasfv  17293  ressbas  17314  firest  17503  topnval  17505  homffval  17764  comfffval  17772  oppchomfval  17788  xpcbas  18252  oduval  18362  oduleval  18363  lubfun  18424  glbfun  18437  odujoin  18480  odumeet  18482  oduclatb  18581  ipopos  18610  isipodrs  18611  plusffval  18722  grpidval  18737  gsum0  18764  ismnd  18817  frmdplusg  18937  frmd0  18943  efmndbas  18954  efmndbasabf  18955  efmndplusg  18963  dfgrp2e  19054  grpinvfval  19069  grpinvfvalALT  19070  grpinvfvi  19073  grpsubfval  19074  grpsubfvalALT  19075  mulgfval  19159  mulgfvalALT  19160  mulgfvi  19163  cntrval  19413  cntzval  19415  cntzrcl  19421  oppgval  19441  oppgplusfval  19442  symgval  19465  lactghmga  19499  psgnfval  19594  odfval  19626  odfvalALT  19627  oppglsm  19736  efgval  19811  mgpval  20243  mgpplusg  20244  ringidval  20289  opprval  20446  opprmulfval  20447  dvdsrval  20469  invrfval  20497  dvrfval  20510  rrgval  20826  staffval  20974  scaffval  21031  islss  21085  sralem  21327  sravsca  21332  sraip  21333  rlmval  21342  rlmsca2  21350  2idlval  21420  zrhval  21687  zlmvsca  21701  chrval  21703  evpmss  21766  ipffval  21828  ocvval  21847  elocv  21848  thlbas  21876  thlle  21877  thloc  21879  pjfval  21886  asclfval  22058  psrbas  22114  psr1val  22376  vr1val  22382  ply1val  22384  ply1basfvi  22430  ply1plusgfvi  22431  psr1sca2  22440  ply1sca2  22443  ply1ascl  22449  evl1fval  22518  evl1fval1  22521  toponsspwpw  23109  istps  23121  tgdif0  23179  indislem  23187  txindislem  23821  fsubbas  24055  filuni  24073  ussval  24447  isusp  24449  nmfval  24776  tngds  24836  tcphval  25408  deg1fval  26268  deg1fvi  26273  uc1pval  26328  mon1pval  26330  ltsval2  27851  ltsintdifex  27856  vtxval  29381  iedgval  29382  vtxvalprc  29426  iedgvalprc  29427  edgval  29430  prcliscplgr  29798  wwlks  30227  wwlksn  30229  clwwlk  30377  clwwlkn  30420  clwwlknonmpo  30483  vafval  31002  bafval  31003  smfval  31004  vsfval  31032  erlval  33618  fracval  33665  fracbas  33666  resvsca  33692  kardval  35598  kardeq0  35602  kard0b  35605  kardcard2b  35611  prclisacycgr  35656  mvtval  36005  mexval  36007  mexval2  36008  mdvval  36009  mrsubfval  36013  msubfval  36029  elmsubrn  36033  mvhfval  36038  mpstval  36040  msrfval  36042  mstaval  36049  mclsrcl  36066  mppsval  36077  mthmval  36080  fvsingle  36423  funpartfv  36450  fullfunfv  36452  rankeq1o  36676  atbase  40096  llnbase  40316  lplnbase  40341  lvolbase  40385  lhpbase  40805  mzpmfp  43511  kelac1  43823  mendbas  43940  mendplusgfval  43941  mendmulrfval  43943  mendvscafval  43946  brfvimex  44785  clsneibex  44861  neicvgbex  44871  sprssspr  48263  sprsymrelfvlem  48272  prprelprb  48299  prprspr2  48300  upwlkbprop  48936  ipolub00  49804  resccat  49885  oppcup3  50020  initopropdlem  50051  termopropdlem  50052  zeroopropdlem  50053  catcrcl  50206