Theorem fvprc 6871

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1567   ∈ wcel 2149  ∃!weu 2602  Vcvv 3463  ∅c0 4294   class class class wbr 5110  ‘cfv 6534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-nul 5268  ax-pr 5402

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-iota 6490  df-fv 6542

This theorem is referenced by:  rnfvprc  6873  dffv3  6875  fvrn0  6907  ndmfv  6911  fv2prc  6921  csbfv  6926  dffv2  6974  brfvopabrbr  6984  fvmpti  6986  fvmptnf  7010  fvmptrabfv  7020  fvunsn  7175  fvmptopab  7463  brfvopab  7465  1stval  7984  2ndval  7985  fipwuni  9382  fipwss  9385  tctr  9703  ranklim  9812  rankuni  9831  alephsing  10256  itunisuc  10399  itunitc  10401  tskmcl  10822  hashfn  14407  s1prc  14638  trclfvg  15048  trclfvcotrg  15049  dfrtrclrec2  15091  rtrclreclem4  15094  dfrtrcl2  15095  strfvss  17243  strfvi  17246  fveqprc  17247  oveqprc  17248  elbasfv  17271  ressbas  17292  firest  17481  topnval  17483  homffval  17742  comfffval  17750  oppchomfval  17766  xpcbas  18230  oduval  18340  oduleval  18341  lubfun  18402  glbfun  18415  odujoin  18458  odumeet  18460  oduclatb  18559  ipopos  18588  isipodrs  18589  plusffval  18700  grpidval  18715  gsum0  18738  ismnd  18791  frmdplusg  18909  frmd0  18915  efmndbas  18926  efmndbasabf  18927  efmndplusg  18935  dfgrp2e  19026  grpinvfval  19041  grpinvfvalALT  19042  grpinvfvi  19045  grpsubfval  19046  grpsubfvalALT  19047  mulgfval  19131  mulgfvalALT  19132  mulgfvi  19135  cntrval  19385  cntzval  19387  cntzrcl  19393  oppgval  19413  oppgplusfval  19414  symgval  19437  lactghmga  19471  psgnfval  19566  odfval  19598  odfvalALT  19599  oppglsm  19708  efgval  19783  mgpval  20215  mgpplusg  20216  ringidval  20261  opprval  20416  opprmulfval  20417  dvdsrval  20439  invrfval  20467  dvrfval  20480  rrgval  20778  staffval  20918  scaffval  20975  islss  21029  sralem  21271  sravsca  21276  sraip  21277  rlmval  21286  rlmsca2  21294  2idlval  21357  zrhval  21622  zlmvsca  21636  chrval  21638  evpmss  21701  ipffval  21763  ocvval  21782  elocv  21783  thlbas  21811  thlle  21812  thloc  21814  pjfval  21821  asclfval  21993  psrbas  22049  psr1val  22311  vr1val  22317  ply1val  22319  ply1basfvi  22365  ply1plusgfvi  22366  psr1sca2  22375  ply1sca2  22378  ply1ascl  22384  evl1fval  22453  evl1fval1  22456  toponsspwpw  23044  istps  23056  tgdif0  23114  indislem  23122  txindislem  23755  fsubbas  23989  filuni  24007  ussval  24381  isusp  24383  nmfval  24710  tngds  24770  tcphval  25342  deg1fval  26202  deg1fvi  26207  uc1pval  26262  mon1pval  26264  ltsval2  27782  ltsintdifex  27787  vtxval  29287  iedgval  29288  vtxvalprc  29332  iedgvalprc  29333  edgval  29336  prcliscplgr  29701  wwlks  30121  wwlksn  30123  clwwlk  30271  clwwlkn  30314  clwwlknonmpo  30377  vafval  30892  bafval  30893  smfval  30894  vsfval  30922  erlval  33515  fracval  33564  fracbas  33565  resvsca  33591  prclisacycgr  35538  mvtval  35887  mexval  35889  mexval2  35890  mdvval  35891  mrsubfval  35895  msubfval  35911  elmsubrn  35915  mvhfval  35920  mpstval  35922  msrfval  35924  mstaval  35931  mclsrcl  35948  mppsval  35959  mthmval  35962  fvsingle  36305  funpartfv  36332  fullfunfv  36334  rankeq1o  36558  atbase  39948  llnbase  40168  lplnbase  40193  lvolbase  40237  lhpbase  40657  mzpmfp  43365  kelac1  43677  mendbas  43794  mendplusgfval  43795  mendmulrfval  43797  mendvscafval  43800  brfvimex  44639  clsneibex  44715  neicvgbex  44725  sprssspr  48114  sprsymrelfvlem  48123  prprelprb  48150  prprspr2  48151  upwlkbprop  48787  ipolub00  49651  resccat  49732  oppcup3  49867  initopropdlem  49898  termopropdlem  49899  zeroopropdlem  49900  catcrcl  50053