Theorem fvprc 6834

Description: A function's value at a proper class is the empty set. See fvprcALT 6835 for a proof that uses ax-pow 5320 instead of ax-pr 5384. (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 6832	. 2 ⊢ (¬ 𝐴 ∈ V → ¬ ∃!𝑥 𝐴𝐹𝑥)
2		tz6.12-2 6830	. 2 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅)
3	1, 2	syl 17	1 ⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ∈ wcel 2106  ∃!weu 2566  Vcvv 3445  ∅c0 4282   class class class wbr 5105  ‘cfv 6496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-nul 5263  ax-pr 5384

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-iota 6448  df-fv 6504

This theorem is referenced by:  rnfvprc  6836  dffv3  6838  fvrn0  6872  ndmfv  6877  fv2prc  6887  csbfv  6892  dffv2  6936  brfvopabrbr  6945  fvmpti  6947  fvmptnf  6970  fvmptrabfv  6979  fvunsn  7125  fvmptopab  7411  fvmptopabOLD  7412  brfvopab  7414  1stval  7923  2ndval  7924  fipwuni  9362  fipwss  9365  tctr  9676  ranklim  9780  rankuni  9799  alephsing  10212  itunisuc  10355  itunitc  10357  tskmcl  10777  hashfn  14275  s1prc  14492  trclfvg  14900  trclfvcotrg  14901  dfrtrclrec2  14943  rtrclreclem4  14946  dfrtrcl2  14947  strfvss  17059  strfvi  17062  fveqprc  17063  oveqprc  17064  setsnidOLD  17082  elbasfv  17089  ressbas  17118  ressbasOLD  17119  resslemOLD  17123  firest  17314  topnval  17316  homffval  17570  comfffval  17578  oppchomfval  17594  oppchomfvalOLD  17595  oppcbasOLD  17600  xpcbas  18066  oduval  18177  oduleval  18178  lubfun  18241  glbfun  18254  odujoin  18297  odumeet  18299  oduclatb  18396  ipopos  18425  isipodrs  18426  plusffval  18503  grpidval  18516  gsum0  18539  ismnd  18559  frmdplusg  18664  frmd0  18670  efmndbas  18681  efmndbasabf  18682  efmndplusg  18690  dfgrp2e  18776  grpinvfval  18789  grpinvfvalALT  18790  grpinvfvi  18793  grpsubfval  18794  grpsubfvalALT  18795  mulgfval  18874  mulgfvalALT  18875  mulgfvi  18878  cntrval  19099  cntzval  19101  cntzrcl  19107  oppgval  19125  oppgplusfval  19126  symgval  19150  lactghmga  19187  psgnfval  19282  odfval  19314  odfvalALT  19315  oppglsm  19424  efgval  19499  mgpval  19899  mgpplusg  19900  ringidval  19915  opprval  20050  opprmulfval  20051  dvdsrval  20074  invrfval  20102  dvrfval  20113  staffval  20306  scaffval  20340  islss  20395  sralem  20638  sralemOLD  20639  sravsca  20648  sravscaOLD  20649  sraip  20650  rlmval  20660  rlmsca2  20670  2idlval  20703  rrgval  20757  zrhval  20908  zlmlemOLD  20918  zlmvsca  20926  chrval  20928  evpmss  20990  ipffval  21052  ocvval  21071  elocv  21072  thlbas  21100  thlbasOLD  21101  thlle  21102  thlleOLD  21103  thloc  21105  pjfval  21112  asclfval  21282  psrbas  21346  psr1val  21557  vr1val  21563  ply1val  21565  ply1basfvi  21612  ply1plusgfvi  21613  psr1sca2  21622  ply1sca2  21625  ply1ascl  21629  evl1fval  21694  evl1fval1  21697  toponsspwpw  22271  istps  22283  tgdif0  22342  indislem  22350  txindislem  22984  fsubbas  23218  filuni  23236  ussval  23611  isusp  23613  nmfval  23944  tnglemOLD  23997  tngds  24011  tngdsOLD  24012  tcphval  24582  deg1fval  25445  deg1fvi  25450  uc1pval  25504  mon1pval  25506  sltval2  27004  sltintdifex  27009  ttglemOLD  27820  vtxval  27951  iedgval  27952  vtxvalprc  27996  iedgvalprc  27997  edgval  28000  prcliscplgr  28362  wwlks  28780  wwlksn  28782  clwwlk  28927  clwwlkn  28970  clwwlknonmpo  29033  vafval  29545  bafval  29546  smfval  29547  vsfval  29575  resvsca  32121  resvlemOLD  32123  prclisacycgr  33745  mvtval  34094  mexval  34096  mexval2  34097  mdvval  34098  mrsubfval  34102  msubfval  34118  elmsubrn  34122  mvhfval  34127  mpstval  34129  msrfval  34131  mstaval  34138  mclsrcl  34155  mppsval  34166  mthmval  34169  fvsingle  34505  funpartfv  34530  fullfunfv  34532  rankeq1o  34756  atbase  37751  llnbase  37972  lplnbase  37997  lvolbase  38041  lhpbase  38461  mzpmfp  41056  kelac1  41376  mendbas  41497  mendplusgfval  41498  mendmulrfval  41500  mendvscafval  41503  brfvimex  42288  clsneibex  42364  neicvgbex  42374  sprssspr  45663  sprsymrelfvlem  45672  prprelprb  45699  prprspr2  45700  upwlkbprop  46030  ipolub00  47008