Theorem fvprc 6823

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ∈ wcel 2113  ∃!weu 2565  Vcvv 3437  ∅c0 4282   class class class wbr 5095  ‘cfv 6489

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 2115  ax-9 2123  ax-ext 2705  ax-nul 5248  ax-pr 5374

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 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-iota 6445  df-fv 6497

This theorem is referenced by:  rnfvprc  6825  dffv3  6827  fvrn0  6859  ndmfv  6863  fv2prc  6873  csbfv  6878  dffv2  6926  brfvopabrbr  6935  fvmpti  6937  fvmptnf  6960  fvmptrabfv  6970  fvunsn  7122  fvmptopab  7410  brfvopab  7412  1stval  7932  2ndval  7933  fipwuni  9321  fipwss  9324  tctr  9639  ranklim  9748  rankuni  9767  alephsing  10178  itunisuc  10321  itunitc  10323  tskmcl  10743  hashfn  14289  s1prc  14519  trclfvg  14929  trclfvcotrg  14930  dfrtrclrec2  14972  rtrclreclem4  14975  dfrtrcl2  14976  strfvss  17105  strfvi  17108  fveqprc  17109  oveqprc  17110  elbasfv  17133  ressbas  17154  firest  17343  topnval  17345  homffval  17604  comfffval  17612  oppchomfval  17628  xpcbas  18092  oduval  18202  oduleval  18203  lubfun  18264  glbfun  18277  odujoin  18320  odumeet  18322  oduclatb  18421  ipopos  18450  isipodrs  18451  plusffval  18562  grpidval  18577  gsum0  18600  ismnd  18653  frmdplusg  18770  frmd0  18776  efmndbas  18787  efmndbasabf  18788  efmndplusg  18796  dfgrp2e  18884  grpinvfval  18899  grpinvfvalALT  18900  grpinvfvi  18903  grpsubfval  18904  grpsubfvalALT  18905  mulgfval  18990  mulgfvalALT  18991  mulgfvi  18994  cntrval  19239  cntzval  19241  cntzrcl  19247  oppgval  19267  oppgplusfval  19268  symgval  19291  lactghmga  19325  psgnfval  19420  odfval  19452  odfvalALT  19453  oppglsm  19562  efgval  19637  mgpval  20069  mgpplusg  20070  ringidval  20109  opprval  20265  opprmulfval  20266  dvdsrval  20288  invrfval  20316  dvrfval  20329  rrgval  20621  staffval  20765  scaffval  20822  islss  20876  sralem  21119  sravsca  21124  sraip  21125  rlmval  21134  rlmsca2  21142  2idlval  21197  zrhval  21453  zlmvsca  21467  chrval  21469  evpmss  21532  ipffval  21594  ocvval  21613  elocv  21614  thlbas  21642  thlle  21643  thloc  21645  pjfval  21652  asclfval  21825  psrbas  21880  psr1val  22117  vr1val  22123  ply1val  22125  ply1basfvi  22172  ply1plusgfvi  22173  psr1sca2  22182  ply1sca2  22185  ply1ascl  22191  evl1fval  22263  evl1fval1  22266  toponsspwpw  22857  istps  22869  tgdif0  22927  indislem  22935  txindislem  23568  fsubbas  23802  filuni  23820  ussval  24194  isusp  24196  nmfval  24523  tngds  24583  tcphval  25165  deg1fval  26032  deg1fvi  26037  uc1pval  26092  mon1pval  26094  sltval2  27615  sltintdifex  27620  vtxval  28999  iedgval  29000  vtxvalprc  29044  iedgvalprc  29045  edgval  29048  prcliscplgr  29413  wwlks  29834  wwlksn  29836  clwwlk  29984  clwwlkn  30027  clwwlknonmpo  30090  vafval  30604  bafval  30605  smfval  30606  vsfval  30634  erlval  33268  fracval  33314  fracbas  33315  resvsca  33341  prclisacycgr  35267  mvtval  35616  mexval  35618  mexval2  35619  mdvval  35620  mrsubfval  35624  msubfval  35640  elmsubrn  35644  mvhfval  35649  mpstval  35651  msrfval  35653  mstaval  35660  mclsrcl  35677  mppsval  35688  mthmval  35691  fvsingle  36034  funpartfv  36061  fullfunfv  36063  rankeq1o  36287  atbase  39461  llnbase  39681  lplnbase  39706  lvolbase  39750  lhpbase  40170  mzpmfp  42904  kelac1  43220  mendbas  43337  mendplusgfval  43338  mendmulrfval  43340  mendvscafval  43343  brfvimex  44183  clsneibex  44259  neicvgbex  44269  sprssspr  47643  sprsymrelfvlem  47652  prprelprb  47679  prprspr2  47680  upwlkbprop  48300  ipolub00  49154  resccat  49235  oppcup3  49370  initopropdlem  49401  termopropdlem  49402  zeroopropdlem  49403  catcrcl  49556