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

Theorem fvprc 5602
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.
StepHypRef Expression
1 brprcneu 5601 . 2  |-  ( -.  A  e.  _V  ->  -.  E! x  A F x )
2 tz6.12-2 5599 . 2  |-  ( -.  E! x  A F x  ->  ( F `  A )  =  (/) )
31, 2syl 15 1  |-  ( -.  A  e.  _V  ->  ( F `  A )  =  (/) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1642    e. wcel 1710   E!weu 2209   _Vcvv 2864   (/)c0 3531   class class class wbr 4104   ` cfv 5337
This theorem is referenced by:  dffv3  5604  fvrn0  5633  ndmfv  5635  dffv2  5675  fvmpti  5684  fvmptnf  5700  fvunsn  5796  1stval  6211  2ndval  6212  riotav  6396  riotaprc  6429  riotassuni  6430  fipwuni  7269  fipwss  7272  tctr  7515  ranklim  7606  rankuni  7625  alephsing  7992  itunisuc  8135  itunitc1  8136  itunitc  8137  tskmcl  8553  hashfn  11450  strfvss  13263  strfvi  13283  setsnid  13285  elbasfv  13288  ressbas  13295  resslem  13298  firest  13436  topnval  13438  homffval  13693  comfffval  13700  oppchomfval  13716  oppcbas  13720  xpcbas  14051  oduval  14333  oduleval  14334  odumeet  14343  odujoin  14345  oduclatb  14347  ipopos  14362  isipodrs  14363  ismnd  14468  plusffval  14478  grpidval  14483  gsum0  14556  frmdplusg  14575  frmd0  14581  grpinvfval  14619  grpinvfvi  14622  grpsubfval  14623  mulgfval  14667  mulgfvi  14670  symgbas  14871  symgplusg  14875  lactghmga  14883  cntrval  14894  cntzval  14896  cntzrcl  14902  oppgval  14919  oppgplusfval  14920  odfval  14947  oppglsm  15052  efgval  15125  mgpval  15427  mgpplusg  15428  rngidval  15442  opprval  15505  opprmulfval  15506  dvdsrval  15526  invrfval  15554  dvrfval  15565  staffval  15711  scaffval  15744  islss  15791  sralem  16029  srasca  16033  sravsca  16034  rlmval  16044  rlmsca2  16052  2idlval  16084  rrgval  16127  asclfval  16173  psrbas  16223  psr1val  16364  vr1val  16370  ply1val  16372  psr1rclOLD  16378  ply1rclOLD  16381  ply1basfvi  16418  ply1plusgfvi  16419  psr1sca2  16428  ply1sca2  16431  ply1ascl  16434  zrhval  16568  zlmlem  16577  zlmvsca  16582  chrval  16585  ipffval  16658  ocvval  16673  elocv  16674  thlbas  16702  thlle  16703  thloc  16705  pjfval  16712  istps  16780  tgclb  16814  tgdif0  16836  indislem  16843  txindislem  17433  fsubbas  17664  filuni  17682  nmfval  18213  tnglem  18258  tngds  18266  tchval  18754  evl1fval  19514  deg1fval  19570  deg1fvi  19575  uc1pval  19629  mon1pval  19631  vafval  21273  bafval  21274  smfval  21275  vsfval  21305  ussval  23558  isusp  23560  sltval2  24868  sltintdifex  24875  funpartfv  25042  fullfunfv  25044  rankeq1o  25360  mzpmfp  26148  kelac1  26484  pmtrfrn  26723  psgnfval  26746  mendbas  26815  mendplusgfval  26816  mendmulrfval  26818  mendsca  26820  mendvscafval  26821  atbase  29548  llnbase  29767  lplnbase  29792  lvolbase  29836  lhpbase  30256
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-nul 4230  ax-pow 4269
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-uni 3909  df-br 4105  df-iota 5301  df-fv 5345
  Copyright terms: Public domain W3C validator