Theorem fvprc 6809

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ∈ wcel 2111  ∃!weu 2563  Vcvv 3436  ∅c0 4278   class class class wbr 5086  ‘cfv 6476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-nul 5239  ax-pr 5365

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-iota 6432  df-fv 6484

This theorem is referenced by:  rnfvprc  6811  dffv3  6813  fvrn0  6845  ndmfv  6849  fv2prc  6859  csbfv  6864  dffv2  6912  brfvopabrbr  6921  fvmpti  6923  fvmptnf  6946  fvmptrabfv  6956  fvunsn  7108  fvmptopab  7396  brfvopab  7398  1stval  7918  2ndval  7919  fipwuni  9305  fipwss  9308  tctr  9623  ranklim  9732  rankuni  9751  alephsing  10162  itunisuc  10305  itunitc  10307  tskmcl  10727  hashfn  14277  s1prc  14507  trclfvg  14917  trclfvcotrg  14918  dfrtrclrec2  14960  rtrclreclem4  14963  dfrtrcl2  14964  strfvss  17093  strfvi  17096  fveqprc  17097  oveqprc  17098  elbasfv  17121  ressbas  17142  firest  17331  topnval  17333  homffval  17591  comfffval  17599  oppchomfval  17615  xpcbas  18079  oduval  18189  oduleval  18190  lubfun  18251  glbfun  18264  odujoin  18307  odumeet  18309  oduclatb  18408  ipopos  18437  isipodrs  18438  plusffval  18549  grpidval  18564  gsum0  18587  ismnd  18640  frmdplusg  18757  frmd0  18763  efmndbas  18774  efmndbasabf  18775  efmndplusg  18783  dfgrp2e  18871  grpinvfval  18886  grpinvfvalALT  18887  grpinvfvi  18890  grpsubfval  18891  grpsubfvalALT  18892  mulgfval  18977  mulgfvalALT  18978  mulgfvi  18981  cntrval  19226  cntzval  19228  cntzrcl  19234  oppgval  19254  oppgplusfval  19255  symgval  19278  lactghmga  19312  psgnfval  19407  odfval  19439  odfvalALT  19440  oppglsm  19549  efgval  19624  mgpval  20056  mgpplusg  20057  ringidval  20096  opprval  20251  opprmulfval  20252  dvdsrval  20274  invrfval  20302  dvrfval  20315  rrgval  20607  staffval  20751  scaffval  20808  islss  20862  sralem  21105  sravsca  21110  sraip  21111  rlmval  21120  rlmsca2  21128  2idlval  21183  zrhval  21439  zlmvsca  21453  chrval  21455  evpmss  21518  ipffval  21580  ocvval  21599  elocv  21600  thlbas  21628  thlle  21629  thloc  21631  pjfval  21638  asclfval  21811  psrbas  21865  psr1val  22093  vr1val  22099  ply1val  22101  ply1basfvi  22148  ply1plusgfvi  22149  psr1sca2  22158  ply1sca2  22161  ply1ascl  22167  evl1fval  22238  evl1fval1  22241  toponsspwpw  22832  istps  22844  tgdif0  22902  indislem  22910  txindislem  23543  fsubbas  23777  filuni  23795  ussval  24169  isusp  24171  nmfval  24498  tngds  24558  tcphval  25140  deg1fval  26007  deg1fvi  26012  uc1pval  26067  mon1pval  26069  sltval2  27590  sltintdifex  27595  vtxval  28973  iedgval  28974  vtxvalprc  29018  iedgvalprc  29019  edgval  29022  prcliscplgr  29387  wwlks  29808  wwlksn  29810  clwwlk  29955  clwwlkn  29998  clwwlknonmpo  30061  vafval  30575  bafval  30576  smfval  30577  vsfval  30605  erlval  33217  fracval  33262  fracbas  33263  resvsca  33289  prclisacycgr  35187  mvtval  35536  mexval  35538  mexval2  35539  mdvval  35540  mrsubfval  35544  msubfval  35560  elmsubrn  35564  mvhfval  35569  mpstval  35571  msrfval  35573  mstaval  35580  mclsrcl  35597  mppsval  35608  mthmval  35611  fvsingle  35954  funpartfv  35979  fullfunfv  35981  rankeq1o  36205  atbase  39328  llnbase  39548  lplnbase  39573  lvolbase  39617  lhpbase  40037  mzpmfp  42780  kelac1  43096  mendbas  43213  mendplusgfval  43214  mendmulrfval  43216  mendvscafval  43219  brfvimex  44059  clsneibex  44135  neicvgbex  44145  sprssspr  47512  sprsymrelfvlem  47521  prprelprb  47548  prprspr2  47549  upwlkbprop  48169  ipolub00  49024  resccat  49106  oppcup3  49241  initopropdlem  49272  termopropdlem  49273  zeroopropdlem  49274  catcrcl  49427