MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fvprc Unicode version

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

Proof of Theorem fvprc
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 brprcneu 5864 . 2
2 tz6.12-2 5862 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  =wceq 1395  e.wcel 1818  E!weu 2282   cvv 3109   c0 3784   class class class wbr 4452  `cfv 5593
This theorem is referenced by:  dffv3  5867  fvrn0  5893  ndmfv  5895  csbfv  5909  dffv2  5946  fvmpti  5955  fvmptnf  5973  fvunsn  6103  1stval  6802  2ndval  6803  fipwuni  7906  fipwss  7909  tctr  8192  ranklim  8283  rankuni  8302  alephsing  8677  itunisuc  8820  itunitc1  8821  itunitc  8822  tskmcl  9240  hashfn  12443  strfvss  14650  strfvi  14672  setsnid  14674  elbasfv  14679  ressbas  14687  resslem  14690  firest  14830  topnval  14832  homffval  15086  comfffval  15093  oppchomfval  15109  oppcbas  15113  xpcbas  15447  lubfun  15610  glbfun  15623  oduval  15760  oduleval  15761  odumeet  15770  odujoin  15772  oduclatb  15774  ipopos  15790  isipodrs  15791  plusffval  15877  grpidval  15887  gsum0  15905  ismnd  15923  ismndOLD  15926  frmdplusg  16022  frmd0  16028  grpinvfval  16088  grpinvfvi  16091  grpsubfval  16092  mulgfval  16143  mulgfvi  16146  cntrval  16357  cntzval  16359  cntzrcl  16365  oppgval  16382  oppgplusfval  16383  symgbas  16405  symgplusg  16414  lactghmga  16429  pmtrfrn  16483  psgnfval  16525  odfval  16557  oppglsm  16662  efgval  16735  mgpval  17144  mgpplusg  17145  ringidval  17155  opprval  17273  opprmulfval  17274  dvdsrval  17294  invrfval  17322  dvrfval  17333  staffval  17496  scaffval  17530  islss  17581  sralem  17823  srasca  17827  sravsca  17828  sraip  17829  rlmval  17837  rlmsca2  17847  2idlval  17881  rrgval  17935  asclfval  17983  psrbas  18030  psrbasOLD  18031  psr1val  18225  vr1val  18231  ply1val  18233  ply1basfvi  18282  ply1plusgfvi  18283  psr1sca2  18292  ply1sca2  18295  ply1ascl  18299  evl1fval  18364  evl1fval1  18367  zrhval  18545  zlmlem  18554  zlmvsca  18559  chrval  18562  evpmss  18622  ipffval  18683  ocvval  18698  elocv  18699  thlbas  18727  thlle  18728  thloc  18730  pjfval  18737  istps  19437  tgdif0  19494  indislem  19501  txindislem  20134  fsubbas  20368  filuni  20386  ussval  20762  isusp  20764  nmfval  21109  tnglem  21154  tngds  21162  tchval  21661  deg1fval  22480  deg1fvi  22485  uc1pval  22540  mon1pval  22542  ttglem  24179  vafval  25496  bafval  25497  smfval  25498  vsfval  25528  resvsca  27820  resvlem  27821  mvtval  28860  mexval  28862  mexval2  28863  mdvval  28864  mrsubfval  28868  mrsubrn  28873  mrsub0  28876  mrsubf  28877  mrsubccat  28878  mrsubcn  28879  mrsubco  28881  mrsubvrs  28882  msubfval  28884  elmsubrn  28888  msubrn  28889  msubf  28892  mvhfval  28893  mpstval  28895  msrfval  28897  mstaval  28904  mclsrcl  28921  mppsval  28932  mthmval  28935  sltval2  29416  sltintdifex  29423  fvsingle  29570  funpartfv  29595  fullfunfv  29597  rankeq1o  29828  mzpmfp  30679  mzpmfpOLD  30680  kelac1  31009  mendbas  31133  mendplusgfval  31134  mendmulrfval  31136  mendsca  31138  mendvscafval  31139  atbase  35014  llnbase  35233  lplnbase  35258  lvolbase  35302  lhpbase  35722
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-nul 4581  ax-pow 4630
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-iota 5556  df-fv 5601
  Copyright terms: Public domain W3C validator