Theorem fvprc 6826

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ∈ wcel 2114  ∃!weu 2569  Vcvv 3430  ∅c0 4274   class class class wbr 5086  ‘cfv 6492

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 2709  ax-nul 5241  ax-pr 5370

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6448  df-fv 6500

This theorem is referenced by:  rnfvprc  6828  dffv3  6830  fvrn0  6862  ndmfv  6866  fv2prc  6876  csbfv  6881  dffv2  6929  brfvopabrbr  6938  fvmpti  6940  fvmptnf  6964  fvmptrabfv  6974  fvunsn  7127  fvmptopab  7415  brfvopab  7417  1stval  7937  2ndval  7938  fipwuni  9332  fipwss  9335  tctr  9650  ranklim  9759  rankuni  9778  alephsing  10189  itunisuc  10332  itunitc  10334  tskmcl  10755  hashfn  14328  s1prc  14558  trclfvg  14968  trclfvcotrg  14969  dfrtrclrec2  15011  rtrclreclem4  15014  dfrtrcl2  15015  strfvss  17148  strfvi  17151  fveqprc  17152  oveqprc  17153  elbasfv  17176  ressbas  17197  firest  17386  topnval  17388  homffval  17647  comfffval  17655  oppchomfval  17671  xpcbas  18135  oduval  18245  oduleval  18246  lubfun  18307  glbfun  18320  odujoin  18363  odumeet  18365  oduclatb  18464  ipopos  18493  isipodrs  18494  plusffval  18605  grpidval  18620  gsum0  18643  ismnd  18696  frmdplusg  18813  frmd0  18819  efmndbas  18830  efmndbasabf  18831  efmndplusg  18839  dfgrp2e  18930  grpinvfval  18945  grpinvfvalALT  18946  grpinvfvi  18949  grpsubfval  18950  grpsubfvalALT  18951  mulgfval  19036  mulgfvalALT  19037  mulgfvi  19040  cntrval  19285  cntzval  19287  cntzrcl  19293  oppgval  19313  oppgplusfval  19314  symgval  19337  lactghmga  19371  psgnfval  19466  odfval  19498  odfvalALT  19499  oppglsm  19608  efgval  19683  mgpval  20115  mgpplusg  20116  ringidval  20155  opprval  20309  opprmulfval  20310  dvdsrval  20332  invrfval  20360  dvrfval  20373  rrgval  20665  staffval  20809  scaffval  20866  islss  20920  sralem  21163  sravsca  21168  sraip  21169  rlmval  21178  rlmsca2  21186  2idlval  21241  zrhval  21497  zlmvsca  21511  chrval  21513  evpmss  21576  ipffval  21638  ocvval  21657  elocv  21658  thlbas  21686  thlle  21687  thloc  21689  pjfval  21696  asclfval  21868  psrbas  21923  psr1val  22159  vr1val  22165  ply1val  22167  ply1basfvi  22214  ply1plusgfvi  22215  psr1sca2  22224  ply1sca2  22227  ply1ascl  22233  evl1fval  22303  evl1fval1  22306  toponsspwpw  22897  istps  22909  tgdif0  22967  indislem  22975  txindislem  23608  fsubbas  23842  filuni  23860  ussval  24234  isusp  24236  nmfval  24563  tngds  24623  tcphval  25195  deg1fval  26055  deg1fvi  26060  uc1pval  26115  mon1pval  26117  ltsval2  27634  ltsintdifex  27639  vtxval  29083  iedgval  29084  vtxvalprc  29128  iedgvalprc  29129  edgval  29132  prcliscplgr  29497  wwlks  29918  wwlksn  29920  clwwlk  30068  clwwlkn  30111  clwwlknonmpo  30174  vafval  30689  bafval  30690  smfval  30691  vsfval  30719  erlval  33334  fracval  33380  fracbas  33381  resvsca  33407  prclisacycgr  35349  mvtval  35698  mexval  35700  mexval2  35701  mdvval  35702  mrsubfval  35706  msubfval  35722  elmsubrn  35726  mvhfval  35731  mpstval  35733  msrfval  35735  mstaval  35742  mclsrcl  35759  mppsval  35770  mthmval  35773  fvsingle  36116  funpartfv  36143  fullfunfv  36145  rankeq1o  36369  atbase  39749  llnbase  39969  lplnbase  39994  lvolbase  40038  lhpbase  40458  mzpmfp  43193  kelac1  43509  mendbas  43626  mendplusgfval  43627  mendmulrfval  43629  mendvscafval  43632  brfvimex  44471  clsneibex  44547  neicvgbex  44557  sprssspr  47953  sprsymrelfvlem  47962  prprelprb  47989  prprspr2  47990  upwlkbprop  48626  ipolub00  49480  resccat  49561  oppcup3  49696  initopropdlem  49727  termopropdlem  49728  zeroopropdlem  49729  catcrcl  49882