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

Theorem fvprc 5842
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 5841 . 2  |-  ( -.  A  e.  _V  ->  -.  E! x  A F x )
2 tz6.12-2 5839 . 2  |-  ( -.  E! x  A F x  ->  ( F `  A )  =  (/) )
31, 2syl 16 1  |-  ( -.  A  e.  _V  ->  ( F `  A )  =  (/) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1398    e. wcel 1823   E!weu 2284   _Vcvv 3106   (/)c0 3783   class class class wbr 4439   ` cfv 5570
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-nul 4568  ax-pow 4615
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-iota 5534  df-fv 5578
This theorem is referenced by:  dffv3  5844  fvrn0  5870  ndmfv  5872  csbfv  5885  dffv2  5921  fvmpti  5930  fvmptnf  5949  fvunsn  6079  1stval  6775  2ndval  6776  fipwuni  7878  fipwss  7881  tctr  8162  ranklim  8253  rankuni  8272  alephsing  8647  itunisuc  8790  itunitc1  8791  itunitc  8792  tskmcl  9208  hashfn  12429  trclfvg  12936  trclfvcotrg  12937  strfvss  14737  strfvi  14761  setsnid  14763  elbasfv  14768  ressbas  14776  resslem  14779  firest  14925  topnval  14927  homffval  15181  comfffval  15189  oppchomfval  15205  oppcbas  15209  xpcbas  15649  lubfun  15812  glbfun  15825  oduval  15962  oduleval  15963  odumeet  15972  odujoin  15974  oduclatb  15976  ipopos  15992  isipodrs  15993  plusffval  16079  grpidval  16089  gsum0  16107  ismnd  16125  ismndOLD  16128  frmdplusg  16224  frmd0  16230  grpinvfval  16290  grpinvfvi  16293  grpsubfval  16294  mulgfval  16345  mulgfvi  16348  cntrval  16559  cntzval  16561  cntzrcl  16567  oppgval  16584  oppgplusfval  16585  symgbas  16607  symgplusg  16616  lactghmga  16631  pmtrfrn  16685  psgnfval  16727  odfval  16759  oppglsm  16864  efgval  16937  mgpval  17342  mgpplusg  17343  ringidval  17353  opprval  17471  opprmulfval  17472  dvdsrval  17492  invrfval  17520  dvrfval  17531  staffval  17694  scaffval  17728  islss  17779  sralem  18021  srasca  18025  sravsca  18026  sraip  18027  rlmval  18035  rlmsca2  18045  2idlval  18079  rrgval  18133  asclfval  18181  psrbas  18228  psrbasOLD  18229  psr1val  18423  vr1val  18429  ply1val  18431  ply1basfvi  18480  ply1plusgfvi  18481  psr1sca2  18490  ply1sca2  18493  ply1ascl  18497  evl1fval  18562  evl1fval1  18565  zrhval  18723  zlmlem  18732  zlmvsca  18737  chrval  18740  evpmss  18798  ipffval  18859  ocvval  18874  elocv  18875  thlbas  18903  thlle  18904  thloc  18906  pjfval  18913  istps  19607  tgdif0  19664  indislem  19671  txindislem  20303  fsubbas  20537  filuni  20555  ussval  20931  isusp  20933  nmfval  21278  tnglem  21323  tngds  21331  tchval  21830  deg1fval  22649  deg1fvi  22654  uc1pval  22709  mon1pval  22711  ttglem  24384  vafval  25697  bafval  25698  smfval  25699  vsfval  25729  resvsca  28058  resvlem  28059  mvtval  29127  mexval  29129  mexval2  29130  mdvval  29131  mrsubfval  29135  mrsubrn  29140  mrsub0  29143  mrsubf  29144  mrsubccat  29145  mrsubcn  29146  mrsubco  29148  mrsubvrs  29149  msubfval  29151  elmsubrn  29155  msubrn  29156  msubf  29159  mvhfval  29160  mpstval  29162  msrfval  29164  mstaval  29171  mclsrcl  29188  mppsval  29199  mthmval  29202  sltval2  29659  sltintdifex  29666  fvsingle  29801  funpartfv  29826  fullfunfv  29828  rankeq1o  30059  mzpmfp  30922  kelac1  31251  mendbas  31377  mendplusgfval  31378  mendmulrfval  31380  mendsca  31382  mendvscafval  31383  atbase  35430  llnbase  35649  lplnbase  35674  lvolbase  35718  lhpbase  36138
  Copyright terms: Public domain W3C validator