Theorem fvprc 6912

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ∈ wcel 2108  ∃!weu 2571  Vcvv 3488  ∅c0 4352   class class class wbr 5166  ‘cfv 6573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581

This theorem is referenced by:  rnfvprc  6914  dffv3  6916  fvrn0  6950  ndmfv  6955  fv2prc  6965  csbfv  6970  dffv2  7017  brfvopabrbr  7026  fvmpti  7028  fvmptnf  7051  fvmptrabfv  7061  fvunsn  7213  fvmptopab  7504  fvmptopabOLD  7505  brfvopab  7507  1stval  8032  2ndval  8033  fipwuni  9495  fipwss  9498  tctr  9809  ranklim  9913  rankuni  9932  alephsing  10345  itunisuc  10488  itunitc  10490  tskmcl  10910  hashfn  14424  s1prc  14652  trclfvg  15064  trclfvcotrg  15065  dfrtrclrec2  15107  rtrclreclem4  15110  dfrtrcl2  15111  strfvss  17234  strfvi  17237  fveqprc  17238  oveqprc  17239  setsnidOLD  17257  elbasfv  17264  ressbas  17293  ressbasOLD  17294  resslemOLD  17301  firest  17492  topnval  17494  homffval  17748  comfffval  17756  oppchomfval  17772  oppchomfvalOLD  17773  oppcbasOLD  17778  xpcbas  18247  oduval  18358  oduleval  18359  lubfun  18422  glbfun  18435  odujoin  18478  odumeet  18480  oduclatb  18577  ipopos  18606  isipodrs  18607  plusffval  18684  grpidval  18699  gsum0  18722  ismnd  18775  frmdplusg  18889  frmd0  18895  efmndbas  18906  efmndbasabf  18907  efmndplusg  18915  dfgrp2e  19003  grpinvfval  19018  grpinvfvalALT  19019  grpinvfvi  19022  grpsubfval  19023  grpsubfvalALT  19024  mulgfval  19109  mulgfvalALT  19110  mulgfvi  19113  cntrval  19359  cntzval  19361  cntzrcl  19367  oppgval  19387  oppgplusfval  19388  symgval  19412  lactghmga  19447  psgnfval  19542  odfval  19574  odfvalALT  19575  oppglsm  19684  efgval  19759  mgpval  20164  mgpplusg  20165  ringidval  20210  opprval  20361  opprmulfval  20362  dvdsrval  20387  invrfval  20415  dvrfval  20428  rrgval  20719  staffval  20864  scaffval  20900  islss  20955  sralem  21198  sralemOLD  21199  sravsca  21208  sravscaOLD  21209  sraip  21210  rlmval  21221  rlmsca2  21229  2idlval  21284  zrhval  21541  zlmlemOLD  21551  zlmvsca  21559  chrval  21561  evpmss  21627  ipffval  21689  ocvval  21708  elocv  21709  thlbas  21737  thlbasOLD  21738  thlle  21739  thlleOLD  21740  thloc  21742  pjfval  21749  asclfval  21922  psrbas  21976  psr1val  22208  vr1val  22214  ply1val  22216  ply1basfvi  22263  ply1plusgfvi  22264  psr1sca2  22273  ply1sca2  22276  ply1ascl  22282  evl1fval  22353  evl1fval1  22356  toponsspwpw  22949  istps  22961  tgdif0  23020  indislem  23028  txindislem  23662  fsubbas  23896  filuni  23914  ussval  24289  isusp  24291  nmfval  24622  tnglemOLD  24675  tngds  24689  tngdsOLD  24690  tcphval  25271  deg1fval  26139  deg1fvi  26144  uc1pval  26199  mon1pval  26201  sltval2  27719  sltintdifex  27724  ttglemOLD  28904  vtxval  29035  iedgval  29036  vtxvalprc  29080  iedgvalprc  29081  edgval  29084  prcliscplgr  29449  wwlks  29868  wwlksn  29870  clwwlk  30015  clwwlkn  30058  clwwlknonmpo  30121  vafval  30635  bafval  30636  smfval  30637  vsfval  30665  erlval  33230  fracval  33271  fracbas  33272  resvsca  33321  resvlemOLD  33323  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  39245  llnbase  39466  lplnbase  39491  lvolbase  39535  lhpbase  39955  mzpmfp  42703  kelac1  43020  mendbas  43141  mendplusgfval  43142  mendmulrfval  43144  mendvscafval  43147  brfvimex  43988  clsneibex  44064  neicvgbex  44074  sprssspr  47355  sprsymrelfvlem  47364  prprelprb  47391  prprspr2  47392  upwlkbprop  47861  ipolub00  48665