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

Theorem fvprc 5875
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 5874 . 2  |-  ( -.  A  e.  _V  ->  -.  E! x  A F x )
2 tz6.12-2 5872 . 2  |-  ( -.  E! x  A F x  ->  ( F `  A )  =  (/) )
31, 2syl 17 1  |-  ( -.  A  e.  _V  ->  ( F `  A )  =  (/) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1437    e. wcel 1870   E!weu 2266   _Vcvv 3087   (/)c0 3767   class class class wbr 4426   ` cfv 5601
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-nul 4556  ax-pow 4603
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-iota 5565  df-fv 5609
This theorem is referenced by:  dffv3  5877  fvrn0  5903  ndmfv  5905  csbfv  5918  dffv2  5954  fvmpti  5963  fvmptnf  5983  fvunsn  6111  1stval  6809  2ndval  6810  fipwuni  7946  fipwss  7949  tctr  8223  ranklim  8314  rankuni  8333  alephsing  8704  itunisuc  8847  itunitc1  8848  itunitc  8849  tskmcl  9265  hashfn  12551  trclfvg  13058  trclfvcotrg  13059  strfvss  15102  strfvi  15126  setsnid  15128  elbasfv  15133  ressbas  15141  resslem  15144  firest  15290  topnval  15292  homffval  15546  comfffval  15554  oppchomfval  15570  oppcbas  15574  xpcbas  16014  lubfun  16177  glbfun  16190  oduval  16327  oduleval  16328  odumeet  16337  odujoin  16339  oduclatb  16341  ipopos  16357  isipodrs  16358  plusffval  16444  grpidval  16454  gsum0  16472  ismnd  16490  ismndOLD  16493  frmdplusg  16589  frmd0  16595  grpinvfval  16655  grpinvfvi  16658  grpsubfval  16659  mulgfval  16710  mulgfvi  16713  cntrval  16924  cntzval  16926  cntzrcl  16932  oppgval  16949  oppgplusfval  16950  symgbas  16972  symgplusg  16981  lactghmga  16996  pmtrfrn  17050  psgnfval  17092  odfval  17124  oppglsm  17229  efgval  17302  mgpval  17661  mgpplusg  17662  ringidval  17672  opprval  17787  opprmulfval  17788  dvdsrval  17808  invrfval  17836  dvrfval  17847  staffval  18010  scaffval  18044  islss  18093  sralem  18335  srasca  18339  sravsca  18340  sraip  18341  rlmval  18349  rlmsca2  18359  2idlval  18392  rrgval  18446  asclfval  18493  psrbas  18537  psr1val  18714  vr1val  18720  ply1val  18722  ply1basfvi  18769  ply1plusgfvi  18770  psr1sca2  18779  ply1sca2  18782  ply1ascl  18786  evl1fval  18851  evl1fval1  18854  zrhval  19010  zlmlem  19019  zlmvsca  19024  chrval  19027  evpmss  19085  ipffval  19146  ocvval  19161  elocv  19162  thlbas  19190  thlle  19191  thloc  19193  pjfval  19200  istps  19882  tgdif0  19939  indislem  19946  txindislem  20579  fsubbas  20813  filuni  20831  ussval  21205  isusp  21207  nmfval  21534  tnglem  21579  tngds  21587  tchval  22085  deg1fval  22906  deg1fvi  22911  uc1pval  22965  mon1pval  22967  ttglem  24752  vafval  26067  bafval  26068  smfval  26069  vsfval  26099  resvsca  28432  resvlem  28433  mvtval  29926  mexval  29928  mexval2  29929  mdvval  29930  mrsubfval  29934  mrsubrn  29939  mrsub0  29942  mrsubf  29943  mrsubccat  29944  mrsubcn  29945  mrsubco  29947  mrsubvrs  29948  msubfval  29950  elmsubrn  29954  msubrn  29955  msubf  29958  mvhfval  29959  mpstval  29961  msrfval  29963  mstaval  29970  mclsrcl  29987  mppsval  29998  mthmval  30001  sltval2  30330  sltintdifex  30337  fvsingle  30472  funpartfv  30497  fullfunfv  30499  rankeq1o  30723  atbase  32563  llnbase  32782  lplnbase  32807  lvolbase  32851  lhpbase  33271  mzpmfp  35297  kelac1  35626  mendbas  35748  mendplusgfval  35749  mendmulrfval  35751  mendsca  35753  mendvscafval  35754
  Copyright terms: Public domain W3C validator