Theorem fvprc 6223

Description: A function's value at a proper class is the empty set. (Contributed by NM, 20-May-1998.)

Assertion

Ref	Expression
fvprc	⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅)

Proof of Theorem fvprc

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		brprcneu 6222	. 2 ⊢ (¬ 𝐴 ∈ V → ¬ ∃!𝑥 𝐴𝐹𝑥)
2		tz6.12-2 6220	. 2 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅)
3	1, 2	syl 17	1 ⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1523   ∈ wcel 2030  ∃!weu 2498  Vcvv 3231  ∅c0 3948   class class class wbr 4685  ‘cfv 5926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-nul 4822  ax-pow 4873

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934

This theorem is referenced by:  dffv3  6225  fvrn0  6254  ndmfv  6256  fv2prc  6266  csbfv  6271  dffv2  6310  brfvopabrbr  6318  fvmpti  6320  fvmptnf  6341  fvmptrabfv  6348  fvunsn  6486  fvmptopab  6739  brfvopab  6742  1stval  7212  2ndval  7213  fipwuni  8373  fipwss  8376  tctr  8654  ranklim  8745  rankuni  8764  alephsing  9136  itunisuc  9279  itunitc1  9280  itunitc  9281  tskmcl  9701  hashfn  13202  s1prc  13420  trclfvg  13800  trclfvcotrg  13801  strfvss  15927  strfvi  15960  setsnid  15962  elbasfv  15967  ressbas  15977  resslem  15980  firest  16140  topnval  16142  homffval  16397  comfffval  16405  oppchomfval  16421  oppcbas  16425  xpcbas  16865  lubfun  17027  glbfun  17040  oduval  17177  oduleval  17178  odumeet  17187  odujoin  17189  oduclatb  17191  ipopos  17207  isipodrs  17208  plusffval  17294  grpidval  17307  gsum0  17325  ismnd  17344  frmdplusg  17438  frmd0  17444  dfgrp2e  17495  grpinvfval  17507  grpinvfvi  17510  grpsubfval  17511  mulgfval  17589  mulgfvi  17592  cntrval  17798  cntzval  17800  cntzrcl  17806  oppgval  17823  oppgplusfval  17824  symgbas  17846  symgplusg  17855  lactghmga  17870  pmtrfrn  17924  psgnfval  17966  odfval  17998  oppglsm  18103  efgval  18176  mgpval  18538  mgpplusg  18539  ringidval  18549  opprval  18670  opprmulfval  18671  dvdsrval  18691  invrfval  18719  dvrfval  18730  staffval  18895  scaffval  18929  islss  18983  sralem  19225  srasca  19229  sravsca  19230  sraip  19231  rlmval  19239  rlmsca2  19249  2idlval  19281  rrgval  19335  asclfval  19382  psrbas  19426  psr1val  19604  vr1val  19610  ply1val  19612  ply1basfvi  19659  ply1plusgfvi  19660  psr1sca2  19669  ply1sca2  19672  ply1ascl  19676  evl1fval  19740  evl1fval1  19743  zrhval  19904  zlmlem  19913  zlmvsca  19918  chrval  19921  evpmss  19980  ipffval  20041  ocvval  20059  elocv  20060  thlbas  20088  thlle  20089  thloc  20091  pjfval  20098  toponsspwpw  20774  istps  20786  tgdif0  20844  indislem  20852  txindislem  21484  fsubbas  21718  filuni  21736  ussval  22110  isusp  22112  nmfval  22440  tnglem  22491  tngds  22499  tchval  23063  deg1fval  23885  deg1fvi  23890  uc1pval  23944  mon1pval  23946  ttglem  25801  vtxval  25923  iedgval  25924  vtxvalprc  25982  iedgvalprc  25983  edgval  25986  prcliscplgr  26365  wwlks  26783  wwlksn  26785  clwwlk  26951  clwwlkn  26985  clwwlknOLD  26986  clwwlknonmpt2  27062  vafval  27586  bafval  27587  smfval  27588  vsfval  27616  resvsca  29958  resvlem  29959  mvtval  31523  mexval  31525  mexval2  31526  mdvval  31527  mrsubfval  31531  mrsubrn  31536  mrsub0  31539  mrsubf  31540  mrsubccat  31541  mrsubcn  31542  mrsubco  31544  mrsubvrs  31545  msubfval  31547  elmsubrn  31551  msubrn  31552  msubf  31555  mvhfval  31556  mpstval  31558  msrfval  31560  mstaval  31567  mclsrcl  31584  mppsval  31595  mthmval  31598  sltval2  31934  sltintdifex  31939  fvsingle  32152  funpartfv  32177  fullfunfv  32179  rankeq1o  32403  atbase  34894  llnbase  35113  lplnbase  35138  lvolbase  35182  lhpbase  35602  mzpmfp  37627  kelac1  37950  mendbas  38071  mendplusgfval  38072  mendmulrfval  38074  mendsca  38076  mendvscafval  38077  brfvimex  38641  clsneibex  38717  neicvgbex  38727  upwlkbprop  42044  sprssspr  42056  sprsymrelfvlem  42065