Theorem fvprc 6775

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ∈ wcel 2107  ∃!weu 2569  Vcvv 3433  ∅c0 4257   class class class wbr 5075  ‘cfv 6437

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 2710  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-iota 6395  df-fv 6445

This theorem is referenced by:  rnfvprc  6777  dffv3  6779  fvrn0  6811  ndmfv  6813  fv2prc  6823  csbfv  6828  dffv2  6872  brfvopabrbr  6881  fvmpti  6883  fvmptnf  6906  fvmptrabfv  6915  fvunsn  7060  fvmptopab  7338  fvmptopabOLD  7339  brfvopab  7341  1stval  7842  2ndval  7843  fipwuni  9194  fipwss  9197  tctr  9507  ranklim  9611  rankuni  9630  alephsing  10041  itunisuc  10184  itunitc  10186  tskmcl  10606  hashfn  14099  s1prc  14318  trclfvg  14735  trclfvcotrg  14736  dfrtrclrec2  14778  rtrclreclem4  14781  dfrtrcl2  14782  strfvss  16897  strfvi  16900  fveqprc  16901  oveqprc  16902  setsnidOLD  16920  elbasfv  16927  ressbas  16956  ressbasOLD  16957  resslemOLD  16961  firest  17152  topnval  17154  homffval  17408  comfffval  17416  oppchomfval  17432  oppchomfvalOLD  17433  oppcbasOLD  17438  xpcbas  17904  oduval  18015  oduleval  18016  lubfun  18079  glbfun  18092  odujoin  18135  odumeet  18137  oduclatb  18234  ipopos  18263  isipodrs  18264  plusffval  18341  grpidval  18354  gsum0  18377  ismnd  18397  frmdplusg  18502  frmd0  18508  efmndbas  18519  efmndbasabf  18520  efmndplusg  18528  dfgrp2e  18614  grpinvfval  18627  grpinvfvalALT  18628  grpinvfvi  18631  grpsubfval  18632  grpsubfvalALT  18633  mulgfval  18711  mulgfvalALT  18712  mulgfvi  18715  cntrval  18934  cntzval  18936  cntzrcl  18942  oppgval  18960  oppgplusfval  18961  symgval  18985  lactghmga  19022  psgnfval  19117  odfval  19149  odfvalALT  19150  oppglsm  19256  efgval  19332  mgpval  19732  mgpplusg  19733  ringidval  19748  opprval  19872  opprmulfval  19873  dvdsrval  19896  invrfval  19924  dvrfval  19935  staffval  20116  scaffval  20150  islss  20205  sralem  20448  sralemOLD  20449  sravsca  20458  sravscaOLD  20459  sraip  20460  rlmval  20470  rlmsca2  20480  2idlval  20513  rrgval  20567  zrhval  20718  zlmlemOLD  20728  zlmvsca  20736  chrval  20738  evpmss  20800  ipffval  20862  ocvval  20881  elocv  20882  thlbas  20910  thlbasOLD  20911  thlle  20912  thlleOLD  20913  thloc  20915  pjfval  20922  asclfval  21092  psrbas  21156  psr1val  21366  vr1val  21372  ply1val  21374  ply1basfvi  21421  ply1plusgfvi  21422  psr1sca2  21431  ply1sca2  21434  ply1ascl  21438  evl1fval  21503  evl1fval1  21506  toponsspwpw  22080  istps  22092  tgdif0  22151  indislem  22159  txindislem  22793  fsubbas  23027  filuni  23045  ussval  23420  isusp  23422  nmfval  23753  tnglemOLD  23806  tngds  23820  tngdsOLD  23821  tcphval  24391  deg1fval  25254  deg1fvi  25259  uc1pval  25313  mon1pval  25315  ttglemOLD  27248  vtxval  27379  iedgval  27380  vtxvalprc  27424  iedgvalprc  27425  edgval  27428  prcliscplgr  27790  wwlks  28209  wwlksn  28211  clwwlk  28356  clwwlkn  28399  clwwlknonmpo  28462  vafval  28974  bafval  28975  smfval  28976  vsfval  29004  resvsca  31538  resvlemOLD  31540  prclisacycgr  33122  mvtval  33471  mexval  33473  mexval2  33474  mdvval  33475  mrsubfval  33479  msubfval  33495  elmsubrn  33499  mvhfval  33504  mpstval  33506  msrfval  33508  mstaval  33515  mclsrcl  33532  mppsval  33543  mthmval  33546  sltval2  33868  sltintdifex  33873  fvsingle  34231  funpartfv  34256  fullfunfv  34258  rankeq1o  34482  atbase  37310  llnbase  37530  lplnbase  37555  lvolbase  37599  lhpbase  38019  mzpmfp  40576  kelac1  40895  mendbas  41016  mendplusgfval  41017  mendmulrfval  41019  mendvscafval  41022  brfvimex  41643  clsneibex  41719  neicvgbex  41729  sprssspr  44944  sprsymrelfvlem  44953  prprelprb  44980  prprspr2  44981  upwlkbprop  45311  ipolub00  46290