Theorem fvprc 6832

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ∈ wcel 2109  ∃!weu 2561  Vcvv 3444  ∅c0 4292   class class class wbr 5102  ‘cfv 6499

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 5256  ax-pr 5382

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507

This theorem is referenced by:  rnfvprc  6834  dffv3  6836  fvrn0  6870  ndmfv  6875  fv2prc  6885  csbfv  6890  dffv2  6938  brfvopabrbr  6947  fvmpti  6949  fvmptnf  6972  fvmptrabfv  6982  fvunsn  7135  fvmptopab  7424  brfvopab  7426  1stval  7949  2ndval  7950  fipwuni  9353  fipwss  9356  tctr  9669  ranklim  9773  rankuni  9792  alephsing  10205  itunisuc  10348  itunitc  10350  tskmcl  10770  hashfn  14316  s1prc  14545  trclfvg  14957  trclfvcotrg  14958  dfrtrclrec2  15000  rtrclreclem4  15003  dfrtrcl2  15004  strfvss  17133  strfvi  17136  fveqprc  17137  oveqprc  17138  elbasfv  17161  ressbas  17182  firest  17371  topnval  17373  homffval  17627  comfffval  17635  oppchomfval  17651  xpcbas  18115  oduval  18225  oduleval  18226  lubfun  18287  glbfun  18300  odujoin  18343  odumeet  18345  oduclatb  18442  ipopos  18471  isipodrs  18472  plusffval  18549  grpidval  18564  gsum0  18587  ismnd  18640  frmdplusg  18757  frmd0  18763  efmndbas  18774  efmndbasabf  18775  efmndplusg  18783  dfgrp2e  18871  grpinvfval  18886  grpinvfvalALT  18887  grpinvfvi  18890  grpsubfval  18891  grpsubfvalALT  18892  mulgfval  18977  mulgfvalALT  18978  mulgfvi  18981  cntrval  19227  cntzval  19229  cntzrcl  19235  oppgval  19255  oppgplusfval  19256  symgval  19277  lactghmga  19311  psgnfval  19406  odfval  19438  odfvalALT  19439  oppglsm  19548  efgval  19623  mgpval  20028  mgpplusg  20029  ringidval  20068  opprval  20223  opprmulfval  20224  dvdsrval  20246  invrfval  20274  dvrfval  20287  rrgval  20582  staffval  20726  scaffval  20762  islss  20816  sralem  21059  sravsca  21064  sraip  21065  rlmval  21074  rlmsca2  21082  2idlval  21137  zrhval  21393  zlmvsca  21407  chrval  21409  evpmss  21471  ipffval  21533  ocvval  21552  elocv  21553  thlbas  21581  thlle  21582  thloc  21584  pjfval  21591  asclfval  21764  psrbas  21818  psr1val  22046  vr1val  22052  ply1val  22054  ply1basfvi  22101  ply1plusgfvi  22102  psr1sca2  22111  ply1sca2  22114  ply1ascl  22120  evl1fval  22191  evl1fval1  22194  toponsspwpw  22785  istps  22797  tgdif0  22855  indislem  22863  txindislem  23496  fsubbas  23730  filuni  23748  ussval  24123  isusp  24125  nmfval  24452  tngds  24512  tcphval  25094  deg1fval  25961  deg1fvi  25966  uc1pval  26021  mon1pval  26023  sltval2  27544  sltintdifex  27549  vtxval  28903  iedgval  28904  vtxvalprc  28948  iedgvalprc  28949  edgval  28952  prcliscplgr  29317  wwlks  29738  wwlksn  29740  clwwlk  29885  clwwlkn  29928  clwwlknonmpo  29991  vafval  30505  bafval  30506  smfval  30507  vsfval  30535  erlval  33182  fracval  33227  fracbas  33228  resvsca  33277  prclisacycgr  35111  mvtval  35460  mexval  35462  mexval2  35463  mdvval  35464  mrsubfval  35468  msubfval  35484  elmsubrn  35488  mvhfval  35493  mpstval  35495  msrfval  35497  mstaval  35504  mclsrcl  35521  mppsval  35532  mthmval  35535  fvsingle  35881  funpartfv  35906  fullfunfv  35908  rankeq1o  36132  atbase  39255  llnbase  39476  lplnbase  39501  lvolbase  39545  lhpbase  39965  mzpmfp  42708  kelac1  43025  mendbas  43142  mendplusgfval  43143  mendmulrfval  43145  mendvscafval  43148  brfvimex  43988  clsneibex  44064  neicvgbex  44074  sprssspr  47455  sprsymrelfvlem  47464  prprelprb  47491  prprspr2  47492  upwlkbprop  48099  ipolub00  48954  resccat  49036  oppcup3  49171  initopropdlem  49202  termopropdlem  49203  zeroopropdlem  49204  catcrcl  49357