Theorem fvprc 6867

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ∈ wcel 2108  ∃!weu 2567  Vcvv 3459  ∅c0 4308   class class class wbr 5119  ‘cfv 6530

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 2707  ax-nul 5276  ax-pr 5402

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538

This theorem is referenced by:  rnfvprc  6869  dffv3  6871  fvrn0  6905  ndmfv  6910  fv2prc  6920  csbfv  6925  dffv2  6973  brfvopabrbr  6982  fvmpti  6984  fvmptnf  7007  fvmptrabfv  7017  fvunsn  7170  fvmptopab  7459  fvmptopabOLD  7460  brfvopab  7462  1stval  7988  2ndval  7989  fipwuni  9436  fipwss  9439  tctr  9752  ranklim  9856  rankuni  9875  alephsing  10288  itunisuc  10431  itunitc  10433  tskmcl  10853  hashfn  14391  s1prc  14620  trclfvg  15032  trclfvcotrg  15033  dfrtrclrec2  15075  rtrclreclem4  15078  dfrtrcl2  15079  strfvss  17204  strfvi  17207  fveqprc  17208  oveqprc  17209  elbasfv  17232  ressbas  17255  firest  17444  topnval  17446  homffval  17700  comfffval  17708  oppchomfval  17724  xpcbas  18188  oduval  18298  oduleval  18299  lubfun  18360  glbfun  18373  odujoin  18416  odumeet  18418  oduclatb  18515  ipopos  18544  isipodrs  18545  plusffval  18622  grpidval  18637  gsum0  18660  ismnd  18713  frmdplusg  18830  frmd0  18836  efmndbas  18847  efmndbasabf  18848  efmndplusg  18856  dfgrp2e  18944  grpinvfval  18959  grpinvfvalALT  18960  grpinvfvi  18963  grpsubfval  18964  grpsubfvalALT  18965  mulgfval  19050  mulgfvalALT  19051  mulgfvi  19054  cntrval  19300  cntzval  19302  cntzrcl  19308  oppgval  19328  oppgplusfval  19329  symgval  19350  lactghmga  19384  psgnfval  19479  odfval  19511  odfvalALT  19512  oppglsm  19621  efgval  19696  mgpval  20101  mgpplusg  20102  ringidval  20141  opprval  20296  opprmulfval  20297  dvdsrval  20319  invrfval  20347  dvrfval  20360  rrgval  20655  staffval  20799  scaffval  20835  islss  20889  sralem  21132  sravsca  21137  sraip  21138  rlmval  21147  rlmsca2  21155  2idlval  21210  zrhval  21466  zlmvsca  21480  chrval  21482  evpmss  21544  ipffval  21606  ocvval  21625  elocv  21626  thlbas  21654  thlle  21655  thloc  21657  pjfval  21664  asclfval  21837  psrbas  21891  psr1val  22119  vr1val  22125  ply1val  22127  ply1basfvi  22174  ply1plusgfvi  22175  psr1sca2  22184  ply1sca2  22187  ply1ascl  22193  evl1fval  22264  evl1fval1  22267  toponsspwpw  22858  istps  22870  tgdif0  22928  indislem  22936  txindislem  23569  fsubbas  23803  filuni  23821  ussval  24196  isusp  24198  nmfval  24525  tngds  24585  tcphval  25168  deg1fval  26035  deg1fvi  26040  uc1pval  26095  mon1pval  26097  sltval2  27618  sltintdifex  27623  vtxval  28925  iedgval  28926  vtxvalprc  28970  iedgvalprc  28971  edgval  28974  prcliscplgr  29339  wwlks  29763  wwlksn  29765  clwwlk  29910  clwwlkn  29953  clwwlknonmpo  30016  vafval  30530  bafval  30531  smfval  30532  vsfval  30560  erlval  33199  fracval  33244  fracbas  33245  resvsca  33294  prclisacycgr  35119  mvtval  35468  mexval  35470  mexval2  35471  mdvval  35472  mrsubfval  35476  msubfval  35492  elmsubrn  35496  mvhfval  35501  mpstval  35503  msrfval  35505  mstaval  35512  mclsrcl  35529  mppsval  35540  mthmval  35543  fvsingle  35884  funpartfv  35909  fullfunfv  35911  rankeq1o  36135  atbase  39253  llnbase  39474  lplnbase  39499  lvolbase  39543  lhpbase  39963  mzpmfp  42717  kelac1  43034  mendbas  43151  mendplusgfval  43152  mendmulrfval  43154  mendvscafval  43157  brfvimex  43997  clsneibex  44073  neicvgbex  44083  sprssspr  47443  sprsymrelfvlem  47452  prprelprb  47479  prprspr2  47480  upwlkbprop  48061  ipolub00  48915  resccat  48989  oppcup3  49090  initopropdlem  49105  termopropdlem  49106  zeroopropdlem  49107