Theorem fvprc 6908

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ∈ wcel 2147  ∃!weu 2596  Vcvv 3454  ∅c0 4281   class class class wbr 5108  ‘cfv 6566

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-nul 5266  ax-pr 5398

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-iota 6520  df-fv 6574

This theorem is used by:  rnfvprc  6910  dffv3  6912  fvrn0  6944  ndmfv  6948  fv2prc  6958  csbfv  6963  dffv2  7011  brfvopabrbr  7021  fvmpti  7023  fvmptnf  7047  fvmptrabfv  7057  fvunsn  7215  fvmptopab  7506  brfvopab  7508  1stval  8037  2ndval  8038  fipwuni  9455  fipwss  9458  tctr  9776  ranklim  9895  rankuni  9916  alephsing  10393  itunisuc  10536  itunitc  10538  tskmcl  10965  hashfn  14560  s1prc  14792  trclfvg  15211  trclfvcotrg  15212  dfrtrclrec2  15254  rtrclreclem4  15257  dfrtrcl2  15258  strfvss  17409  strfvi  17412  fveqprc  17413  oveqprc  17414  elbasfv  17437  ressbas  17458  firest  17653  topnval  17655  homffval  17914  comfffval  17922  oppchomfval  17938  xpcbas  18402  oduval  18512  oduleval  18513  lubfun  18574  glbfun  18587  odujoin  18630  odumeet  18632  oduclatb  18731  ipopos  18760  isipodrs  18761  plusffval  18872  grpidval  18890  gsum0  18923  ismnd  18976  frmdplusg  19100  frmd0  19106  efmndbas  19117  efmndbasabf  19118  efmndplusg  19126  dfgrp2e  19224  grpinvfval  19239  grpinvfvalALT  19240  grpinvfvi  19243  grpsubfval  19244  grpsubfvalALT  19245  mulgfval  19329  mulgfvalALT  19330  mulgfvi  19333  cntrval  19584  cntzval  19586  cntzrcl  19592  oppgval  19612  oppgplusfval  19613  symgval  19636  lactghmga  19670  psgnfval  19765  odfval  19797  odfvalALT  19798  oppglsm  19907  efgval  19982  mgpval  20414  mgpplusg  20415  ringidval  20460  opprval  20619  opprmulfval  20620  dvdsrval  20642  invrfval  20670  dvrfval  20683  rrgval  21000  staffval  21149  scaffval  21206  islss  21260  sralem  21502  sravsca  21507  sraip  21508  rlmval  21517  rlmsca2  21525  2idlval  21595  zrhval  21868  zlmvsca  21882  chrval  21884  evpmss  21947  ipffval  22009  ocvval  22028  elocv  22029  thlbas  22057  thlle  22058  thloc  22060  pjfval  22067  asclfval  22241  psrbas  22297  psr1val  22559  vr1val  22565  ply1val  22567  ply1basfvi  22613  ply1plusgfvi  22614  psr1sca2  22623  ply1sca2  22626  ply1ascl  22632  evl1fval  22701  evl1fval1  22704  toponsspwpw  23295  istps  23307  tgdif0  23365  indislem  23373  txindislem  24007  fsubbas  24241  filuni  24259  ussval  24633  isusp  24635  nmfval  24962  tngds  25022  tcphval  25594  deg1fval  26453  deg1fvi  26458  uc1pval  26513  mon1pval  26515  ltsval2  28070  ltsintdifex  28075  vtxval  29635  iedgval  29636  vtxvalprc  29680  iedgvalprc  29681  edgval  29684  prcliscplgr  30052  wwlks  30481  wwlksn  30483  clwwlk  30631  clwwlkn  30674  clwwlknonmpo  30737  vafval  31262  bafval  31263  smfval  31264  vsfval  31292  erlval  33918  fracval  33970  fracbas  33971  resvsca  33997  kardval  35961  kardeq0  35965  kard0b  35968  kardcard2b  35974  prclisacycgr  36114  mvtval  36473  mexval  36475  mexval2  36476  mdvval  36477  mrsubfval  36481  msubfval  36497  elmsubrn  36501  mvhfval  36506  mpstval  36508  msrfval  36510  mstaval  36517  mclsrcl  36534  mppsval  36545  mthmval  36548  fvsingle  36897  funpartfv  36924  fullfunfv  36926  rankeq1o  37147  atbase  40612  llnbase  40832  lplnbase  40857  lvolbase  40901  lhpbase  41321  mzpmfp  44024  kelac1  44331  mendbas  44443  mendplusgfval  44444  mendmulrfval  44446  mendvscafval  44449  brfvimex  45287  clsneibex  45363  neicvgbex  45373  sprssspr  48836  sprsymrelfvlem  48845  prprelprb  48872  prprspr2  48873  upwlkbprop  49509  ipolub00  50438  resccat  50519  oppcup3  50656  initopropdlem  50693  termopropdlem  50694  zeroopropdlem  50695  catcrcl  50861