Theorem fvprc 6898

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ∈ wcel 2108  ∃!weu 2568  Vcvv 3480  ∅c0 4333   class class class wbr 5143  ‘cfv 6561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569

This theorem is referenced by:  rnfvprc  6900  dffv3  6902  fvrn0  6936  ndmfv  6941  fv2prc  6951  csbfv  6956  dffv2  7004  brfvopabrbr  7013  fvmpti  7015  fvmptnf  7038  fvmptrabfv  7048  fvunsn  7199  fvmptopab  7487  fvmptopabOLD  7488  brfvopab  7490  1stval  8016  2ndval  8017  fipwuni  9466  fipwss  9469  tctr  9780  ranklim  9884  rankuni  9903  alephsing  10316  itunisuc  10459  itunitc  10461  tskmcl  10881  hashfn  14414  s1prc  14642  trclfvg  15054  trclfvcotrg  15055  dfrtrclrec2  15097  rtrclreclem4  15100  dfrtrcl2  15101  strfvss  17224  strfvi  17227  fveqprc  17228  oveqprc  17229  setsnidOLD  17246  elbasfv  17253  ressbas  17280  ressbasOLD  17281  resslemOLD  17288  firest  17477  topnval  17479  homffval  17733  comfffval  17741  oppchomfval  17757  xpcbas  18223  oduval  18333  oduleval  18334  lubfun  18397  glbfun  18410  odujoin  18453  odumeet  18455  oduclatb  18552  ipopos  18581  isipodrs  18582  plusffval  18659  grpidval  18674  gsum0  18697  ismnd  18750  frmdplusg  18867  frmd0  18873  efmndbas  18884  efmndbasabf  18885  efmndplusg  18893  dfgrp2e  18981  grpinvfval  18996  grpinvfvalALT  18997  grpinvfvi  19000  grpsubfval  19001  grpsubfvalALT  19002  mulgfval  19087  mulgfvalALT  19088  mulgfvi  19091  cntrval  19337  cntzval  19339  cntzrcl  19345  oppgval  19365  oppgplusfval  19366  symgval  19388  lactghmga  19423  psgnfval  19518  odfval  19550  odfvalALT  19551  oppglsm  19660  efgval  19735  mgpval  20140  mgpplusg  20141  ringidval  20180  opprval  20335  opprmulfval  20336  dvdsrval  20361  invrfval  20389  dvrfval  20402  rrgval  20697  staffval  20842  scaffval  20878  islss  20932  sralem  21175  sralemOLD  21176  sravsca  21185  sravscaOLD  21186  sraip  21187  rlmval  21198  rlmsca2  21206  2idlval  21261  zrhval  21518  zlmlemOLD  21528  zlmvsca  21536  chrval  21538  evpmss  21604  ipffval  21666  ocvval  21685  elocv  21686  thlbas  21714  thlbasOLD  21715  thlle  21716  thlleOLD  21717  thloc  21719  pjfval  21726  asclfval  21899  psrbas  21953  psr1val  22187  vr1val  22193  ply1val  22195  ply1basfvi  22242  ply1plusgfvi  22243  psr1sca2  22252  ply1sca2  22255  ply1ascl  22261  evl1fval  22332  evl1fval1  22335  toponsspwpw  22928  istps  22940  tgdif0  22999  indislem  23007  txindislem  23641  fsubbas  23875  filuni  23893  ussval  24268  isusp  24270  nmfval  24601  tnglemOLD  24654  tngds  24668  tngdsOLD  24669  tcphval  25252  deg1fval  26119  deg1fvi  26124  uc1pval  26179  mon1pval  26181  sltval2  27701  sltintdifex  27706  ttglemOLD  28886  vtxval  29017  iedgval  29018  vtxvalprc  29062  iedgvalprc  29063  edgval  29066  prcliscplgr  29431  wwlks  29855  wwlksn  29857  clwwlk  30002  clwwlkn  30045  clwwlknonmpo  30108  vafval  30622  bafval  30623  smfval  30624  vsfval  30652  erlval  33262  fracval  33306  fracbas  33307  resvsca  33356  resvlemOLD  33358  prclisacycgr  35156  mvtval  35505  mexval  35507  mexval2  35508  mdvval  35509  mrsubfval  35513  msubfval  35529  elmsubrn  35533  mvhfval  35538  mpstval  35540  msrfval  35542  mstaval  35549  mclsrcl  35566  mppsval  35577  mthmval  35580  fvsingle  35921  funpartfv  35946  fullfunfv  35948  rankeq1o  36172  atbase  39290  llnbase  39511  lplnbase  39536  lvolbase  39580  lhpbase  40000  mzpmfp  42758  kelac1  43075  mendbas  43192  mendplusgfval  43193  mendmulrfval  43195  mendvscafval  43198  brfvimex  44039  clsneibex  44115  neicvgbex  44125  sprssspr  47468  sprsymrelfvlem  47477  prprelprb  47504  prprspr2  47505  upwlkbprop  48054  ipolub00  48882