Theorem fvprc 6818

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ∈ wcel 2109  ∃!weu 2561  Vcvv 3438  ∅c0 4286   class class class wbr 5095  ‘cfv 6486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494

This theorem is referenced by:  rnfvprc  6820  dffv3  6822  fvrn0  6854  ndmfv  6859  fv2prc  6869  csbfv  6874  dffv2  6922  brfvopabrbr  6931  fvmpti  6933  fvmptnf  6956  fvmptrabfv  6966  fvunsn  7119  fvmptopab  7408  brfvopab  7410  1stval  7933  2ndval  7934  fipwuni  9335  fipwss  9338  tctr  9655  ranklim  9759  rankuni  9778  alephsing  10189  itunisuc  10332  itunitc  10334  tskmcl  10754  hashfn  14301  s1prc  14530  trclfvg  14941  trclfvcotrg  14942  dfrtrclrec2  14984  rtrclreclem4  14987  dfrtrcl2  14988  strfvss  17117  strfvi  17120  fveqprc  17121  oveqprc  17122  elbasfv  17145  ressbas  17166  firest  17355  topnval  17357  homffval  17615  comfffval  17623  oppchomfval  17639  xpcbas  18103  oduval  18213  oduleval  18214  lubfun  18275  glbfun  18288  odujoin  18331  odumeet  18333  oduclatb  18432  ipopos  18461  isipodrs  18462  plusffval  18539  grpidval  18554  gsum0  18577  ismnd  18630  frmdplusg  18747  frmd0  18753  efmndbas  18764  efmndbasabf  18765  efmndplusg  18773  dfgrp2e  18861  grpinvfval  18876  grpinvfvalALT  18877  grpinvfvi  18880  grpsubfval  18881  grpsubfvalALT  18882  mulgfval  18967  mulgfvalALT  18968  mulgfvi  18971  cntrval  19217  cntzval  19219  cntzrcl  19225  oppgval  19245  oppgplusfval  19246  symgval  19269  lactghmga  19303  psgnfval  19398  odfval  19430  odfvalALT  19431  oppglsm  19540  efgval  19615  mgpval  20047  mgpplusg  20048  ringidval  20087  opprval  20242  opprmulfval  20243  dvdsrval  20265  invrfval  20293  dvrfval  20306  rrgval  20601  staffval  20745  scaffval  20802  islss  20856  sralem  21099  sravsca  21104  sraip  21105  rlmval  21114  rlmsca2  21122  2idlval  21177  zrhval  21433  zlmvsca  21447  chrval  21449  evpmss  21512  ipffval  21574  ocvval  21593  elocv  21594  thlbas  21622  thlle  21623  thloc  21625  pjfval  21632  asclfval  21805  psrbas  21859  psr1val  22087  vr1val  22093  ply1val  22095  ply1basfvi  22142  ply1plusgfvi  22143  psr1sca2  22152  ply1sca2  22155  ply1ascl  22161  evl1fval  22232  evl1fval1  22235  toponsspwpw  22826  istps  22838  tgdif0  22896  indislem  22904  txindislem  23537  fsubbas  23771  filuni  23789  ussval  24164  isusp  24166  nmfval  24493  tngds  24553  tcphval  25135  deg1fval  26002  deg1fvi  26007  uc1pval  26062  mon1pval  26064  sltval2  27585  sltintdifex  27590  vtxval  28964  iedgval  28965  vtxvalprc  29009  iedgvalprc  29010  edgval  29013  prcliscplgr  29378  wwlks  29799  wwlksn  29801  clwwlk  29946  clwwlkn  29989  clwwlknonmpo  30052  vafval  30566  bafval  30567  smfval  30568  vsfval  30596  erlval  33217  fracval  33262  fracbas  33263  resvsca  33289  prclisacycgr  35143  mvtval  35492  mexval  35494  mexval2  35495  mdvval  35496  mrsubfval  35500  msubfval  35516  elmsubrn  35520  mvhfval  35525  mpstval  35527  msrfval  35529  mstaval  35536  mclsrcl  35553  mppsval  35564  mthmval  35567  fvsingle  35913  funpartfv  35938  fullfunfv  35940  rankeq1o  36164  atbase  39287  llnbase  39508  lplnbase  39533  lvolbase  39577  lhpbase  39997  mzpmfp  42740  kelac1  43056  mendbas  43173  mendplusgfval  43174  mendmulrfval  43176  mendvscafval  43179  brfvimex  44019  clsneibex  44095  neicvgbex  44105  sprssspr  47485  sprsymrelfvlem  47494  prprelprb  47521  prprspr2  47522  upwlkbprop  48142  ipolub00  48997  resccat  49079  oppcup3  49214  initopropdlem  49245  termopropdlem  49246  zeroopropdlem  49247  catcrcl  49400