Theorem fvprc 6814

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ∈ wcel 2109  ∃!weu 2561  Vcvv 3436  ∅c0 4284   class class class wbr 5092  ‘cfv 6482

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 5245  ax-pr 5371

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490

This theorem is referenced by:  rnfvprc  6816  dffv3  6818  fvrn0  6850  ndmfv  6855  fv2prc  6865  csbfv  6870  dffv2  6918  brfvopabrbr  6927  fvmpti  6929  fvmptnf  6952  fvmptrabfv  6962  fvunsn  7115  fvmptopab  7404  brfvopab  7406  1stval  7926  2ndval  7927  fipwuni  9316  fipwss  9319  tctr  9636  ranklim  9740  rankuni  9759  alephsing  10170  itunisuc  10313  itunitc  10315  tskmcl  10735  hashfn  14282  s1prc  14511  trclfvg  14922  trclfvcotrg  14923  dfrtrclrec2  14965  rtrclreclem4  14968  dfrtrcl2  14969  strfvss  17098  strfvi  17101  fveqprc  17102  oveqprc  17103  elbasfv  17126  ressbas  17147  firest  17336  topnval  17338  homffval  17596  comfffval  17604  oppchomfval  17620  xpcbas  18084  oduval  18194  oduleval  18195  lubfun  18256  glbfun  18269  odujoin  18312  odumeet  18314  oduclatb  18413  ipopos  18442  isipodrs  18443  plusffval  18520  grpidval  18535  gsum0  18558  ismnd  18611  frmdplusg  18728  frmd0  18734  efmndbas  18745  efmndbasabf  18746  efmndplusg  18754  dfgrp2e  18842  grpinvfval  18857  grpinvfvalALT  18858  grpinvfvi  18861  grpsubfval  18862  grpsubfvalALT  18863  mulgfval  18948  mulgfvalALT  18949  mulgfvi  18952  cntrval  19198  cntzval  19200  cntzrcl  19206  oppgval  19226  oppgplusfval  19227  symgval  19250  lactghmga  19284  psgnfval  19379  odfval  19411  odfvalALT  19412  oppglsm  19521  efgval  19596  mgpval  20028  mgpplusg  20029  ringidval  20068  opprval  20223  opprmulfval  20224  dvdsrval  20246  invrfval  20274  dvrfval  20287  rrgval  20582  staffval  20726  scaffval  20783  islss  20837  sralem  21080  sravsca  21085  sraip  21086  rlmval  21095  rlmsca2  21103  2idlval  21158  zrhval  21414  zlmvsca  21428  chrval  21430  evpmss  21493  ipffval  21555  ocvval  21574  elocv  21575  thlbas  21603  thlle  21604  thloc  21606  pjfval  21613  asclfval  21786  psrbas  21840  psr1val  22068  vr1val  22074  ply1val  22076  ply1basfvi  22123  ply1plusgfvi  22124  psr1sca2  22133  ply1sca2  22136  ply1ascl  22142  evl1fval  22213  evl1fval1  22216  toponsspwpw  22807  istps  22819  tgdif0  22877  indislem  22885  txindislem  23518  fsubbas  23752  filuni  23770  ussval  24145  isusp  24147  nmfval  24474  tngds  24534  tcphval  25116  deg1fval  25983  deg1fvi  25988  uc1pval  26043  mon1pval  26045  sltval2  27566  sltintdifex  27571  vtxval  28945  iedgval  28946  vtxvalprc  28990  iedgvalprc  28991  edgval  28994  prcliscplgr  29359  wwlks  29780  wwlksn  29782  clwwlk  29927  clwwlkn  29970  clwwlknonmpo  30033  vafval  30547  bafval  30548  smfval  30549  vsfval  30577  erlval  33198  fracval  33243  fracbas  33244  resvsca  33270  prclisacycgr  35124  mvtval  35473  mexval  35475  mexval2  35476  mdvval  35477  mrsubfval  35481  msubfval  35497  elmsubrn  35501  mvhfval  35506  mpstval  35508  msrfval  35510  mstaval  35517  mclsrcl  35534  mppsval  35545  mthmval  35548  fvsingle  35894  funpartfv  35919  fullfunfv  35921  rankeq1o  36145  atbase  39268  llnbase  39488  lplnbase  39513  lvolbase  39557  lhpbase  39977  mzpmfp  42720  kelac1  43036  mendbas  43153  mendplusgfval  43154  mendmulrfval  43156  mendvscafval  43159  brfvimex  43999  clsneibex  44075  neicvgbex  44085  sprssspr  47465  sprsymrelfvlem  47474  prprelprb  47501  prprspr2  47502  upwlkbprop  48122  ipolub00  48977  resccat  49059  oppcup3  49194  initopropdlem  49225  termopropdlem  49226  zeroopropdlem  49227  catcrcl  49380