Theorem fvprc 6881

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ∈ wcel 2107  ∃!weu 2563  Vcvv 3475  ∅c0 4322   class class class wbr 5148  ‘cfv 6541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6493  df-fv 6549

This theorem is referenced by:  rnfvprc  6883  dffv3  6885  fvrn0  6919  ndmfv  6924  fv2prc  6934  csbfv  6939  dffv2  6984  brfvopabrbr  6993  fvmpti  6995  fvmptnf  7018  fvmptrabfv  7027  fvunsn  7174  fvmptopab  7460  fvmptopabOLD  7461  brfvopab  7463  1stval  7974  2ndval  7975  fipwuni  9418  fipwss  9421  tctr  9732  ranklim  9836  rankuni  9855  alephsing  10268  itunisuc  10411  itunitc  10413  tskmcl  10833  hashfn  14332  s1prc  14551  trclfvg  14959  trclfvcotrg  14960  dfrtrclrec2  15002  rtrclreclem4  15005  dfrtrcl2  15006  strfvss  17117  strfvi  17120  fveqprc  17121  oveqprc  17122  setsnidOLD  17140  elbasfv  17147  ressbas  17176  ressbasOLD  17177  resslemOLD  17184  firest  17375  topnval  17377  homffval  17631  comfffval  17639  oppchomfval  17655  oppchomfvalOLD  17656  oppcbasOLD  17661  xpcbas  18127  oduval  18238  oduleval  18239  lubfun  18302  glbfun  18315  odujoin  18358  odumeet  18360  oduclatb  18457  ipopos  18486  isipodrs  18487  plusffval  18564  grpidval  18577  gsum0  18600  ismnd  18625  frmdplusg  18732  frmd0  18738  efmndbas  18749  efmndbasabf  18750  efmndplusg  18758  dfgrp2e  18845  grpinvfval  18860  grpinvfvalALT  18861  grpinvfvi  18864  grpsubfval  18865  grpsubfvalALT  18866  mulgfval  18947  mulgfvalALT  18948  mulgfvi  18951  cntrval  19178  cntzval  19180  cntzrcl  19186  oppgval  19206  oppgplusfval  19207  symgval  19231  lactghmga  19268  psgnfval  19363  odfval  19395  odfvalALT  19396  oppglsm  19505  efgval  19580  mgpval  19985  mgpplusg  19986  ringidval  20001  opprval  20144  opprmulfval  20145  dvdsrval  20168  invrfval  20196  dvrfval  20209  staffval  20448  scaffval  20483  islss  20538  sralem  20783  sralemOLD  20784  sravsca  20793  sravscaOLD  20794  sraip  20795  rlmval  20806  rlmsca2  20816  2idlval  20851  rrgval  20896  zrhval  21049  zlmlemOLD  21059  zlmvsca  21067  chrval  21069  evpmss  21131  ipffval  21193  ocvval  21212  elocv  21213  thlbas  21241  thlbasOLD  21242  thlle  21243  thlleOLD  21244  thloc  21246  pjfval  21253  asclfval  21425  psrbas  21489  psr1val  21702  vr1val  21708  ply1val  21710  ply1basfvi  21755  ply1plusgfvi  21756  psr1sca2  21765  ply1sca2  21768  ply1ascl  21772  evl1fval  21839  evl1fval1  21842  toponsspwpw  22416  istps  22428  tgdif0  22487  indislem  22495  txindislem  23129  fsubbas  23363  filuni  23381  ussval  23756  isusp  23758  nmfval  24089  tnglemOLD  24142  tngds  24156  tngdsOLD  24157  tcphval  24727  deg1fval  25590  deg1fvi  25595  uc1pval  25649  mon1pval  25651  sltval2  27149  sltintdifex  27154  ttglemOLD  28119  vtxval  28250  iedgval  28251  vtxvalprc  28295  iedgvalprc  28296  edgval  28299  prcliscplgr  28661  wwlks  29079  wwlksn  29081  clwwlk  29226  clwwlkn  29269  clwwlknonmpo  29332  vafval  29844  bafval  29845  smfval  29846  vsfval  29874  resvsca  32433  resvlemOLD  32435  prclisacycgr  34131  mvtval  34480  mexval  34482  mexval2  34483  mdvval  34484  mrsubfval  34488  msubfval  34504  elmsubrn  34508  mvhfval  34513  mpstval  34515  msrfval  34517  mstaval  34524  mclsrcl  34541  mppsval  34552  mthmval  34555  fvsingle  34881  funpartfv  34906  fullfunfv  34908  rankeq1o  35132  atbase  38148  llnbase  38369  lplnbase  38394  lvolbase  38438  lhpbase  38858  mzpmfp  41471  kelac1  41791  mendbas  41912  mendplusgfval  41913  mendmulrfval  41915  mendvscafval  41918  brfvimex  42763  clsneibex  42839  neicvgbex  42849  sprssspr  46136  sprsymrelfvlem  46145  prprelprb  46172  prprspr2  46173  upwlkbprop  46503  ipolub00  47572