Theorem fvprc 6873

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1570   ∈ wcel 2143  ∃!weu 2596  Vcvv 3455  ∅c0 4286   class class class wbr 5109  ‘cfv 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-nul 5269  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544

This theorem is referenced by:  rnfvprc  6875  dffv3  6877  fvrn0  6909  ndmfv  6913  fv2prc  6923  csbfv  6928  dffv2  6976  brfvopabrbr  6986  fvmpti  6988  fvmptnf  7012  fvmptrabfv  7022  fvunsn  7177  fvmptopab  7465  brfvopab  7467  1stval  7984  2ndval  7985  fipwuni  9382  fipwss  9385  tctr  9703  ranklim  9812  rankuni  9831  alephsing  10255  itunisuc  10398  itunitc  10400  tskmcl  10821  hashfn  14407  s1prc  14638  trclfvg  15048  trclfvcotrg  15049  dfrtrclrec2  15091  rtrclreclem4  15094  dfrtrcl2  15095  strfvss  17242  strfvi  17245  fveqprc  17246  oveqprc  17247  elbasfv  17270  ressbas  17291  firest  17480  topnval  17482  homffval  17741  comfffval  17749  oppchomfval  17765  xpcbas  18229  oduval  18339  oduleval  18340  lubfun  18401  glbfun  18414  odujoin  18457  odumeet  18459  oduclatb  18558  ipopos  18587  isipodrs  18588  plusffval  18699  grpidval  18714  gsum0  18737  ismnd  18790  frmdplusg  18908  frmd0  18914  efmndbas  18925  efmndbasabf  18926  efmndplusg  18934  dfgrp2e  19025  grpinvfval  19040  grpinvfvalALT  19041  grpinvfvi  19044  grpsubfval  19045  grpsubfvalALT  19046  mulgfval  19130  mulgfvalALT  19131  mulgfvi  19134  cntrval  19384  cntzval  19386  cntzrcl  19392  oppgval  19412  oppgplusfval  19413  symgval  19436  lactghmga  19470  psgnfval  19565  odfval  19597  odfvalALT  19598  oppglsm  19707  efgval  19782  mgpval  20214  mgpplusg  20215  ringidval  20260  opprval  20416  opprmulfval  20417  dvdsrval  20439  invrfval  20467  dvrfval  20480  rrgval  20796  staffval  20944  scaffval  21001  islss  21055  sralem  21297  sravsca  21302  sraip  21303  rlmval  21312  rlmsca2  21320  2idlval  21390  zrhval  21657  zlmvsca  21671  chrval  21673  evpmss  21736  ipffval  21798  ocvval  21817  elocv  21818  thlbas  21846  thlle  21847  thloc  21849  pjfval  21856  asclfval  22028  psrbas  22084  psr1val  22346  vr1val  22352  ply1val  22354  ply1basfvi  22400  ply1plusgfvi  22401  psr1sca2  22410  ply1sca2  22413  ply1ascl  22419  evl1fval  22488  evl1fval1  22491  toponsspwpw  23079  istps  23091  tgdif0  23149  indislem  23157  txindislem  23790  fsubbas  24024  filuni  24042  ussval  24416  isusp  24418  nmfval  24745  tngds  24805  tcphval  25377  deg1fval  26237  deg1fvi  26242  uc1pval  26297  mon1pval  26299  ltsval2  27820  ltsintdifex  27825  vtxval  29350  iedgval  29351  vtxvalprc  29395  iedgvalprc  29396  edgval  29399  prcliscplgr  29764  wwlks  30184  wwlksn  30186  clwwlk  30334  clwwlkn  30377  clwwlknonmpo  30440  vafval  30955  bafval  30956  smfval  30957  vsfval  30985  erlval  33578  fracval  33625  fracbas  33626  resvsca  33652  kardval  35565  kardeq0  35569  kard0b  35572  kardcard2b  35578  prclisacycgr  35643  mvtval  35992  mexval  35994  mexval2  35995  mdvval  35996  mrsubfval  36000  msubfval  36016  elmsubrn  36020  mvhfval  36025  mpstval  36027  msrfval  36029  mstaval  36036  mclsrcl  36053  mppsval  36064  mthmval  36067  fvsingle  36410  funpartfv  36437  fullfunfv  36439  rankeq1o  36663  atbase  40063  llnbase  40283  lplnbase  40308  lvolbase  40352  lhpbase  40772  mzpmfp  43478  kelac1  43790  mendbas  43907  mendplusgfval  43908  mendmulrfval  43910  mendvscafval  43913  brfvimex  44752  clsneibex  44828  neicvgbex  44838  sprssspr  48230  sprsymrelfvlem  48239  prprelprb  48266  prprspr2  48267  upwlkbprop  48903  ipolub00  49771  resccat  49852  oppcup3  49987  initopropdlem  50018  termopropdlem  50019  zeroopropdlem  50020  catcrcl  50173