Theorem fvprc 6850

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ∈ wcel 2109  ∃!weu 2561  Vcvv 3447  ∅c0 4296   class class class wbr 5107  ‘cfv 6511

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519

This theorem is referenced by:  rnfvprc  6852  dffv3  6854  fvrn0  6888  ndmfv  6893  fv2prc  6903  csbfv  6908  dffv2  6956  brfvopabrbr  6965  fvmpti  6967  fvmptnf  6990  fvmptrabfv  7000  fvunsn  7153  fvmptopab  7443  fvmptopabOLD  7444  brfvopab  7446  1stval  7970  2ndval  7971  fipwuni  9377  fipwss  9380  tctr  9693  ranklim  9797  rankuni  9816  alephsing  10229  itunisuc  10372  itunitc  10374  tskmcl  10794  hashfn  14340  s1prc  14569  trclfvg  14981  trclfvcotrg  14982  dfrtrclrec2  15024  rtrclreclem4  15027  dfrtrcl2  15028  strfvss  17157  strfvi  17160  fveqprc  17161  oveqprc  17162  elbasfv  17185  ressbas  17206  firest  17395  topnval  17397  homffval  17651  comfffval  17659  oppchomfval  17675  xpcbas  18139  oduval  18249  oduleval  18250  lubfun  18311  glbfun  18324  odujoin  18367  odumeet  18369  oduclatb  18466  ipopos  18495  isipodrs  18496  plusffval  18573  grpidval  18588  gsum0  18611  ismnd  18664  frmdplusg  18781  frmd0  18787  efmndbas  18798  efmndbasabf  18799  efmndplusg  18807  dfgrp2e  18895  grpinvfval  18910  grpinvfvalALT  18911  grpinvfvi  18914  grpsubfval  18915  grpsubfvalALT  18916  mulgfval  19001  mulgfvalALT  19002  mulgfvi  19005  cntrval  19251  cntzval  19253  cntzrcl  19259  oppgval  19279  oppgplusfval  19280  symgval  19301  lactghmga  19335  psgnfval  19430  odfval  19462  odfvalALT  19463  oppglsm  19572  efgval  19647  mgpval  20052  mgpplusg  20053  ringidval  20092  opprval  20247  opprmulfval  20248  dvdsrval  20270  invrfval  20298  dvrfval  20311  rrgval  20606  staffval  20750  scaffval  20786  islss  20840  sralem  21083  sravsca  21088  sraip  21089  rlmval  21098  rlmsca2  21106  2idlval  21161  zrhval  21417  zlmvsca  21431  chrval  21433  evpmss  21495  ipffval  21557  ocvval  21576  elocv  21577  thlbas  21605  thlle  21606  thloc  21608  pjfval  21615  asclfval  21788  psrbas  21842  psr1val  22070  vr1val  22076  ply1val  22078  ply1basfvi  22125  ply1plusgfvi  22126  psr1sca2  22135  ply1sca2  22138  ply1ascl  22144  evl1fval  22215  evl1fval1  22218  toponsspwpw  22809  istps  22821  tgdif0  22879  indislem  22887  txindislem  23520  fsubbas  23754  filuni  23772  ussval  24147  isusp  24149  nmfval  24476  tngds  24536  tcphval  25118  deg1fval  25985  deg1fvi  25990  uc1pval  26045  mon1pval  26047  sltval2  27568  sltintdifex  27573  vtxval  28927  iedgval  28928  vtxvalprc  28972  iedgvalprc  28973  edgval  28976  prcliscplgr  29341  wwlks  29765  wwlksn  29767  clwwlk  29912  clwwlkn  29955  clwwlknonmpo  30018  vafval  30532  bafval  30533  smfval  30534  vsfval  30562  erlval  33209  fracval  33254  fracbas  33255  resvsca  33304  prclisacycgr  35138  mvtval  35487  mexval  35489  mexval2  35490  mdvval  35491  mrsubfval  35495  msubfval  35511  elmsubrn  35515  mvhfval  35520  mpstval  35522  msrfval  35524  mstaval  35531  mclsrcl  35548  mppsval  35559  mthmval  35562  fvsingle  35908  funpartfv  35933  fullfunfv  35935  rankeq1o  36159  atbase  39282  llnbase  39503  lplnbase  39528  lvolbase  39572  lhpbase  39992  mzpmfp  42735  kelac1  43052  mendbas  43169  mendplusgfval  43170  mendmulrfval  43172  mendvscafval  43175  brfvimex  44015  clsneibex  44091  neicvgbex  44101  sprssspr  47482  sprsymrelfvlem  47491  prprelprb  47518  prprspr2  47519  upwlkbprop  48126  ipolub00  48981  resccat  49063  oppcup3  49198  initopropdlem  49229  termopropdlem  49230  zeroopropdlem  49231  catcrcl  49384