Theorem fvprc 6185

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

Assertion

Ref	Expression
fvprc	|- ( -. A e. _V -> ( F ` A ) = (/) )

Proof of Theorem fvprc

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		brprcneu 6184	. 2 |- ( -. A e. _V -> -. E! x A F x )
2		tz6.12-2 6182	. 2 |- ( -. E! x A F x -> ( F ` A ) = (/) )
3	1, 2	syl 17	1 |- ( -. A e. _V -> ( F ` A ) = (/) )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1483   e. wcel 1990   E!weu 2470   _Vcvv 3200   (/)c0 3915   class class class wbr 4653   ` cfv 5888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-nul 4789  ax-pow 4843

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896

This theorem is referenced by:  dffv3  6187  fvrn0  6216  ndmfv  6218  fv2prc  6228  csbfv  6233  dffv2  6271  brfvopabrbr  6279  fvmpti  6281  fvmptnf  6302  fvunsn  6445  fvmptopab  6697  brfvopab  6700  1stval  7170  2ndval  7171  fipwuni  8332  fipwss  8335  tctr  8616  ranklim  8707  rankuni  8726  alephsing  9098  itunisuc  9241  itunitc1  9242  itunitc  9243  tskmcl  9663  hashfn  13164  trclfvg  13756  trclfvcotrg  13757  strfvss  15880  strfvi  15913  setsnid  15915  elbasfv  15920  ressbas  15930  resslem  15933  firest  16093  topnval  16095  homffval  16350  comfffval  16358  oppchomfval  16374  oppcbas  16378  xpcbas  16818  lubfun  16980  glbfun  16993  oduval  17130  oduleval  17131  odumeet  17140  odujoin  17142  oduclatb  17144  ipopos  17160  isipodrs  17161  plusffval  17247  grpidval  17260  gsum0  17278  ismnd  17297  frmdplusg  17391  frmd0  17397  dfgrp2e  17448  grpinvfval  17460  grpinvfvi  17463  grpsubfval  17464  mulgfval  17542  mulgfvi  17545  cntrval  17752  cntzval  17754  cntzrcl  17760  oppgval  17777  oppgplusfval  17778  symgbas  17800  symgplusg  17809  lactghmga  17824  pmtrfrn  17878  psgnfval  17920  odfval  17952  oppglsm  18057  efgval  18130  mgpval  18492  mgpplusg  18493  ringidval  18503  opprval  18624  opprmulfval  18625  dvdsrval  18645  invrfval  18673  dvrfval  18684  staffval  18847  scaffval  18881  islss  18935  sralem  19177  srasca  19181  sravsca  19182  sraip  19183  rlmval  19191  rlmsca2  19201  2idlval  19233  rrgval  19287  asclfval  19334  psrbas  19378  psr1val  19556  vr1val  19562  ply1val  19564  ply1basfvi  19611  ply1plusgfvi  19612  psr1sca2  19621  ply1sca2  19624  ply1ascl  19628  evl1fval  19692  evl1fval1  19695  zrhval  19856  zlmlem  19865  zlmvsca  19870  chrval  19873  evpmss  19932  ipffval  19993  ocvval  20011  elocv  20012  thlbas  20040  thlle  20041  thloc  20043  pjfval  20050  toponsspwpw  20726  istps  20738  tgdif0  20796  indislem  20804  txindislem  21436  fsubbas  21671  filuni  21689  ussval  22063  isusp  22065  nmfval  22393  tnglem  22444  tngds  22452  tchval  23017  deg1fval  23840  deg1fvi  23845  uc1pval  23899  mon1pval  23901  ttglem  25756  vtxval  25878  iedgval  25879  vtxvalprc  25937  iedgvalprc  25938  edgval  25941  uvtxa0  26294  uvtxa01vtx  26298  wwlks  26727  wwlksn  26729  clwwlks  26879  clwwlksn  26881  vafval  27458  bafval  27459  smfval  27460  vsfval  27488  resvsca  29830  resvlem  29831  mvtval  31397  mexval  31399  mexval2  31400  mdvval  31401  mrsubfval  31405  mrsubrn  31410  mrsub0  31413  mrsubf  31414  mrsubccat  31415  mrsubcn  31416  mrsubco  31418  mrsubvrs  31419  msubfval  31421  elmsubrn  31425  msubrn  31426  msubf  31429  mvhfval  31430  mpstval  31432  msrfval  31434  mstaval  31441  mclsrcl  31458  mppsval  31469  mthmval  31472  sltval2  31809  sltintdifex  31814  fvsingle  32027  funpartfv  32052  fullfunfv  32054  rankeq1o  32278  atbase  34576  llnbase  34795  lplnbase  34820  lvolbase  34864  lhpbase  35284  mzpmfp  37310  kelac1  37633  mendbas  37754  mendplusgfval  37755  mendmulrfval  37757  mendsca  37759  mendvscafval  37760  brfvimex  38324  clsneibex  38400  neicvgbex  38410  upwlkbprop  41719  sprssspr  41731  sprsymrelfvlem  41740