Theorem fvprc 6853

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ∈ wcel 2109  ∃!weu 2562  Vcvv 3450  ∅c0 4299   class class class wbr 5110  ‘cfv 6514

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 2702  ax-nul 5264  ax-pr 5390

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522

This theorem is referenced by:  rnfvprc  6855  dffv3  6857  fvrn0  6891  ndmfv  6896  fv2prc  6906  csbfv  6911  dffv2  6959  brfvopabrbr  6968  fvmpti  6970  fvmptnf  6993  fvmptrabfv  7003  fvunsn  7156  fvmptopab  7446  fvmptopabOLD  7447  brfvopab  7449  1stval  7973  2ndval  7974  fipwuni  9384  fipwss  9387  tctr  9700  ranklim  9804  rankuni  9823  alephsing  10236  itunisuc  10379  itunitc  10381  tskmcl  10801  hashfn  14347  s1prc  14576  trclfvg  14988  trclfvcotrg  14989  dfrtrclrec2  15031  rtrclreclem4  15034  dfrtrcl2  15035  strfvss  17164  strfvi  17167  fveqprc  17168  oveqprc  17169  elbasfv  17192  ressbas  17213  firest  17402  topnval  17404  homffval  17658  comfffval  17666  oppchomfval  17682  xpcbas  18146  oduval  18256  oduleval  18257  lubfun  18318  glbfun  18331  odujoin  18374  odumeet  18376  oduclatb  18473  ipopos  18502  isipodrs  18503  plusffval  18580  grpidval  18595  gsum0  18618  ismnd  18671  frmdplusg  18788  frmd0  18794  efmndbas  18805  efmndbasabf  18806  efmndplusg  18814  dfgrp2e  18902  grpinvfval  18917  grpinvfvalALT  18918  grpinvfvi  18921  grpsubfval  18922  grpsubfvalALT  18923  mulgfval  19008  mulgfvalALT  19009  mulgfvi  19012  cntrval  19258  cntzval  19260  cntzrcl  19266  oppgval  19286  oppgplusfval  19287  symgval  19308  lactghmga  19342  psgnfval  19437  odfval  19469  odfvalALT  19470  oppglsm  19579  efgval  19654  mgpval  20059  mgpplusg  20060  ringidval  20099  opprval  20254  opprmulfval  20255  dvdsrval  20277  invrfval  20305  dvrfval  20318  rrgval  20613  staffval  20757  scaffval  20793  islss  20847  sralem  21090  sravsca  21095  sraip  21096  rlmval  21105  rlmsca2  21113  2idlval  21168  zrhval  21424  zlmvsca  21438  chrval  21440  evpmss  21502  ipffval  21564  ocvval  21583  elocv  21584  thlbas  21612  thlle  21613  thloc  21615  pjfval  21622  asclfval  21795  psrbas  21849  psr1val  22077  vr1val  22083  ply1val  22085  ply1basfvi  22132  ply1plusgfvi  22133  psr1sca2  22142  ply1sca2  22145  ply1ascl  22151  evl1fval  22222  evl1fval1  22225  toponsspwpw  22816  istps  22828  tgdif0  22886  indislem  22894  txindislem  23527  fsubbas  23761  filuni  23779  ussval  24154  isusp  24156  nmfval  24483  tngds  24543  tcphval  25125  deg1fval  25992  deg1fvi  25997  uc1pval  26052  mon1pval  26054  sltval2  27575  sltintdifex  27580  vtxval  28934  iedgval  28935  vtxvalprc  28979  iedgvalprc  28980  edgval  28983  prcliscplgr  29348  wwlks  29772  wwlksn  29774  clwwlk  29919  clwwlkn  29962  clwwlknonmpo  30025  vafval  30539  bafval  30540  smfval  30541  vsfval  30569  erlval  33216  fracval  33261  fracbas  33262  resvsca  33311  prclisacycgr  35145  mvtval  35494  mexval  35496  mexval2  35497  mdvval  35498  mrsubfval  35502  msubfval  35518  elmsubrn  35522  mvhfval  35527  mpstval  35529  msrfval  35531  mstaval  35538  mclsrcl  35555  mppsval  35566  mthmval  35569  fvsingle  35915  funpartfv  35940  fullfunfv  35942  rankeq1o  36166  atbase  39289  llnbase  39510  lplnbase  39535  lvolbase  39579  lhpbase  39999  mzpmfp  42742  kelac1  43059  mendbas  43176  mendplusgfval  43177  mendmulrfval  43179  mendvscafval  43182  brfvimex  44022  clsneibex  44098  neicvgbex  44108  sprssspr  47486  sprsymrelfvlem  47495  prprelprb  47522  prprspr2  47523  upwlkbprop  48130  ipolub00  48985  resccat  49067  oppcup3  49202  initopropdlem  49233  termopropdlem  49234  zeroopropdlem  49235  catcrcl  49388