Theorem fvprc 6875

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ∈ wcel 2145  ∃!weu 2594  Vcvv 3451  ∅c0 4279   class class class wbr 5103  ‘cfv 6537

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-nul 5260  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6493  df-fv 6545

This theorem is used by:  rnfvprc  6877  dffv3  6879  fvrn0  6911  ndmfv  6915  fv2prc  6925  csbfv  6930  dffv2  6978  brfvopabrbr  6988  fvmpti  6990  fvmptnf  7014  fvmptrabfv  7024  fvunsn  7182  fvmptopab  7473  brfvopab  7475  1stval  8001  2ndval  8002  fipwuni  9411  fipwss  9414  tctr  9732  ranklim  9851  rankuni  9872  alephsing  10347  itunisuc  10490  itunitc  10492  tskmcl  10919  hashfn  14512  s1prc  14744  trclfvg  15161  trclfvcotrg  15162  dfrtrclrec2  15204  rtrclreclem4  15207  dfrtrcl2  15208  strfvss  17358  strfvi  17361  fveqprc  17362  oveqprc  17363  elbasfv  17386  ressbas  17407  firest  17596  topnval  17598  homffval  17857  comfffval  17865  oppchomfval  17881  xpcbas  18345  oduval  18455  oduleval  18456  lubfun  18517  glbfun  18530  odujoin  18573  odumeet  18575  oduclatb  18674  ipopos  18703  isipodrs  18704  plusffval  18815  grpidval  18833  gsum0  18866  ismnd  18919  frmdplusg  19043  frmd0  19049  efmndbas  19060  efmndbasabf  19061  efmndplusg  19069  dfgrp2e  19167  grpinvfval  19182  grpinvfvalALT  19183  grpinvfvi  19186  grpsubfval  19187  grpsubfvalALT  19188  mulgfval  19272  mulgfvalALT  19273  mulgfvi  19276  cntrval  19526  cntzval  19528  cntzrcl  19534  oppgval  19554  oppgplusfval  19555  symgval  19578  lactghmga  19612  psgnfval  19707  odfval  19739  odfvalALT  19740  oppglsm  19849  efgval  19924  mgpval  20356  mgpplusg  20357  ringidval  20402  opprval  20561  opprmulfval  20562  dvdsrval  20584  invrfval  20612  dvrfval  20625  rrgval  20942  staffval  21091  scaffval  21148  islss  21202  sralem  21444  sravsca  21449  sraip  21450  rlmval  21459  rlmsca2  21467  2idlval  21537  zrhval  21806  zlmvsca  21820  chrval  21822  evpmss  21885  ipffval  21947  ocvval  21966  elocv  21967  thlbas  21995  thlle  21996  thloc  21998  pjfval  22005  asclfval  22179  psrbas  22235  psr1val  22497  vr1val  22503  ply1val  22505  ply1basfvi  22551  ply1plusgfvi  22552  psr1sca2  22561  ply1sca2  22564  ply1ascl  22570  evl1fval  22639  evl1fval1  22642  toponsspwpw  23233  istps  23245  tgdif0  23303  indislem  23311  txindislem  23945  fsubbas  24179  filuni  24197  ussval  24571  isusp  24573  nmfval  24900  tngds  24960  tcphval  25532  deg1fval  26391  deg1fvi  26396  uc1pval  26451  mon1pval  26453  ltsval2  28006  ltsintdifex  28011  vtxval  29571  iedgval  29572  vtxvalprc  29616  iedgvalprc  29617  edgval  29620  prcliscplgr  29988  wwlks  30417  wwlksn  30419  clwwlk  30567  clwwlkn  30610  clwwlknonmpo  30673  vafval  31198  bafval  31199  smfval  31200  vsfval  31228  erlval  33812  fracval  33859  fracbas  33860  resvsca  33886  kardval  35803  kardeq0  35807  kard0b  35810  kardcard2b  35816  prclisacycgr  35895  mvtval  36244  mexval  36246  mexval2  36247  mdvval  36248  mrsubfval  36252  msubfval  36268  elmsubrn  36272  mvhfval  36277  mpstval  36279  msrfval  36281  mstaval  36288  mclsrcl  36305  mppsval  36316  mthmval  36319  fvsingle  36662  funpartfv  36689  fullfunfv  36691  rankeq1o  36912  atbase  40326  llnbase  40546  lplnbase  40571  lvolbase  40615  lhpbase  41035  mzpmfp  43737  kelac1  44049  mendbas  44166  mendplusgfval  44167  mendmulrfval  44169  mendvscafval  44172  brfvimex  45011  clsneibex  45087  neicvgbex  45097  sprssspr  48532  sprsymrelfvlem  48541  prprelprb  48568  prprspr2  48569  upwlkbprop  49205  ipolub00  50070  resccat  50151  oppcup3  50286  initopropdlem  50317  termopropdlem  50318  zeroopropdlem  50319  catcrcl  50472