Theorem fvprc 6893

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1534   ∈ wcel 2099  ∃!weu 2557  Vcvv 3462  ∅c0 4325   class class class wbr 5153  ‘cfv 6554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-nul 5311  ax-pr 5433

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-dif 3950  df-un 3952  df-ss 3964  df-nul 4326  df-if 4534  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-br 5154  df-iota 6506  df-fv 6562

This theorem is referenced by:  rnfvprc  6895  dffv3  6897  fvrn0  6931  ndmfv  6936  fv2prc  6946  csbfv  6951  dffv2  6997  brfvopabrbr  7006  fvmpti  7008  fvmptnf  7031  fvmptrabfv  7041  fvunsn  7193  fvmptopab  7479  fvmptopabOLD  7480  brfvopab  7482  1stval  8005  2ndval  8006  fipwuni  9469  fipwss  9472  tctr  9783  ranklim  9887  rankuni  9906  alephsing  10319  itunisuc  10462  itunitc  10464  tskmcl  10884  hashfn  14392  s1prc  14612  trclfvg  15020  trclfvcotrg  15021  dfrtrclrec2  15063  rtrclreclem4  15066  dfrtrcl2  15067  strfvss  17189  strfvi  17192  fveqprc  17193  oveqprc  17194  setsnidOLD  17212  elbasfv  17219  ressbas  17248  ressbasOLD  17249  resslemOLD  17256  firest  17447  topnval  17449  homffval  17703  comfffval  17711  oppchomfval  17727  oppchomfvalOLD  17728  oppcbasOLD  17733  xpcbas  18202  oduval  18313  oduleval  18314  lubfun  18377  glbfun  18390  odujoin  18433  odumeet  18435  oduclatb  18532  ipopos  18561  isipodrs  18562  plusffval  18639  grpidval  18654  gsum0  18677  ismnd  18730  frmdplusg  18844  frmd0  18850  efmndbas  18861  efmndbasabf  18862  efmndplusg  18870  dfgrp2e  18958  grpinvfval  18973  grpinvfvalALT  18974  grpinvfvi  18977  grpsubfval  18978  grpsubfvalALT  18979  mulgfval  19063  mulgfvalALT  19064  mulgfvi  19067  cntrval  19313  cntzval  19315  cntzrcl  19321  oppgval  19341  oppgplusfval  19342  symgval  19366  lactghmga  19403  psgnfval  19498  odfval  19530  odfvalALT  19531  oppglsm  19640  efgval  19715  mgpval  20120  mgpplusg  20121  ringidval  20166  opprval  20317  opprmulfval  20318  dvdsrval  20343  invrfval  20371  dvrfval  20384  rrgval  20675  staffval  20820  scaffval  20856  islss  20911  sralem  21154  sralemOLD  21155  sravsca  21164  sravscaOLD  21165  sraip  21166  rlmval  21177  rlmsca2  21185  2idlval  21240  zrhval  21497  zlmlemOLD  21507  zlmvsca  21515  chrval  21517  evpmss  21582  ipffval  21644  ocvval  21663  elocv  21664  thlbas  21692  thlbasOLD  21693  thlle  21694  thlleOLD  21695  thloc  21697  pjfval  21704  asclfval  21876  psrbas  21942  psr1val  22175  vr1val  22181  ply1val  22183  ply1basfvi  22230  ply1plusgfvi  22231  psr1sca2  22240  ply1sca2  22243  ply1ascl  22249  evl1fval  22319  evl1fval1  22322  toponsspwpw  22915  istps  22927  tgdif0  22986  indislem  22994  txindislem  23628  fsubbas  23862  filuni  23880  ussval  24255  isusp  24257  nmfval  24588  tnglemOLD  24641  tngds  24655  tngdsOLD  24656  tcphval  25237  deg1fval  26107  deg1fvi  26112  uc1pval  26167  mon1pval  26169  sltval2  27686  sltintdifex  27691  ttglemOLD  28805  vtxval  28936  iedgval  28937  vtxvalprc  28981  iedgvalprc  28982  edgval  28985  prcliscplgr  29350  wwlks  29769  wwlksn  29771  clwwlk  29916  clwwlkn  29959  clwwlknonmpo  30022  vafval  30536  bafval  30537  smfval  30538  vsfval  30566  erlval  33113  fracval  33154  fracbas  33155  resvsca  33204  resvlemOLD  33206  prclisacycgr  34979  mvtval  35328  mexval  35330  mexval2  35331  mdvval  35332  mrsubfval  35336  msubfval  35352  elmsubrn  35356  mvhfval  35361  mpstval  35363  msrfval  35365  mstaval  35372  mclsrcl  35389  mppsval  35400  mthmval  35403  fvsingle  35744  funpartfv  35769  fullfunfv  35771  rankeq1o  35995  atbase  38987  llnbase  39208  lplnbase  39233  lvolbase  39277  lhpbase  39697  mzpmfp  42404  kelac1  42724  mendbas  42845  mendplusgfval  42846  mendmulrfval  42848  mendvscafval  42851  brfvimex  43693  clsneibex  43769  neicvgbex  43779  sprssspr  47053  sprsymrelfvlem  47062  prprelprb  47089  prprspr2  47090  upwlkbprop  47515  ipolub00  48319