Theorem fvprc 6854

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1559   ∈ wcel 2141  ∃!weu 2594  Vcvv 3453  ∅c0 4283   class class class wbr 5097  ‘cfv 6516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-nul 5253  ax-pr 5387

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-iota 6472  df-fv 6524

This theorem is referenced by:  rnfvprc  6856  dffv3  6858  fvrn0  6890  ndmfv  6894  fv2prc  6904  csbfv  6909  dffv2  6957  brfvopabrbr  6967  fvmpti  6969  fvmptnf  6993  fvmptrabfv  7003  fvunsn  7158  fvmptopab  7446  brfvopab  7448  1stval  7967  2ndval  7968  fipwuni  9366  fipwss  9369  tctr  9687  ranklim  9796  rankuni  9815  alephsing  10227  itunisuc  10370  itunitc  10372  tskmcl  10793  hashfn  14382  s1prc  14612  trclfvg  15022  trclfvcotrg  15023  dfrtrclrec2  15065  rtrclreclem4  15068  dfrtrcl2  15069  strfvss  17214  strfvi  17217  fveqprc  17218  oveqprc  17219  elbasfv  17242  ressbas  17263  firest  17452  topnval  17454  homffval  17713  comfffval  17721  oppchomfval  17737  xpcbas  18201  oduval  18311  oduleval  18312  lubfun  18373  glbfun  18386  odujoin  18429  odumeet  18431  oduclatb  18530  ipopos  18559  isipodrs  18560  plusffval  18671  grpidval  18686  gsum0  18709  ismnd  18762  frmdplusg  18879  frmd0  18885  efmndbas  18896  efmndbasabf  18897  efmndplusg  18905  dfgrp2e  18996  grpinvfval  19011  grpinvfvalALT  19012  grpinvfvi  19015  grpsubfval  19016  grpsubfvalALT  19017  mulgfval  19102  mulgfvalALT  19103  mulgfvi  19106  cntrval  19350  cntzval  19352  cntzrcl  19358  oppgval  19378  oppgplusfval  19379  symgval  19402  lactghmga  19436  psgnfval  19531  odfval  19563  odfvalALT  19564  oppglsm  19673  efgval  19748  mgpval  20180  mgpplusg  20181  ringidval  20220  opprval  20374  opprmulfval  20375  dvdsrval  20397  invrfval  20425  dvrfval  20438  rrgval  20734  staffval  20878  scaffval  20935  islss  20989  sralem  21231  sravsca  21236  sraip  21237  rlmval  21246  rlmsca2  21254  2idlval  21309  zrhval  21547  zlmvsca  21561  chrval  21563  evpmss  21626  ipffval  21688  ocvval  21707  elocv  21708  thlbas  21736  thlle  21737  thloc  21739  pjfval  21746  asclfval  21918  psrbas  21974  psr1val  22236  vr1val  22242  ply1val  22244  ply1basfvi  22290  ply1plusgfvi  22291  psr1sca2  22300  ply1sca2  22303  ply1ascl  22309  evl1fval  22379  evl1fval1  22382  toponsspwpw  22970  istps  22982  tgdif0  23040  indislem  23048  txindislem  23681  fsubbas  23915  filuni  23933  ussval  24307  isusp  24309  nmfval  24636  tngds  24696  tcphval  25268  deg1fval  26128  deg1fvi  26133  uc1pval  26188  mon1pval  26190  ltsval2  27708  ltsintdifex  27713  vtxval  29158  iedgval  29159  vtxvalprc  29203  iedgvalprc  29204  edgval  29207  prcliscplgr  29572  wwlks  29992  wwlksn  29994  clwwlk  30142  clwwlkn  30185  clwwlknonmpo  30248  vafval  30763  bafval  30764  smfval  30765  vsfval  30793  erlval  33400  fracval  33452  fracbas  33453  resvsca  33479  prclisacycgr  35462  mvtval  35811  mexval  35813  mexval2  35814  mdvval  35815  mrsubfval  35819  msubfval  35835  elmsubrn  35839  mvhfval  35844  mpstval  35846  msrfval  35848  mstaval  35855  mclsrcl  35872  mppsval  35883  mthmval  35886  fvsingle  36229  funpartfv  36256  fullfunfv  36258  rankeq1o  36482  atbase  39874  llnbase  40094  lplnbase  40119  lvolbase  40163  lhpbase  40583  mzpmfp  43289  kelac1  43601  mendbas  43718  mendplusgfval  43719  mendmulrfval  43721  mendvscafval  43724  brfvimex  44563  clsneibex  44639  neicvgbex  44649  sprssspr  48048  sprsymrelfvlem  48057  prprelprb  48084  prprspr2  48085  upwlkbprop  48721  ipolub00  49575  resccat  49656  oppcup3  49791  initopropdlem  49822  termopropdlem  49823  zeroopropdlem  49824  catcrcl  49977