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

Theorem fvprc 5846
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 5845 . 2  |-  ( -.  A  e.  _V  ->  -.  E! x  A F x )
2 tz6.12-2 5843 . 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 1381    e. wcel 1802   E!weu 2266   _Vcvv 3093   (/)c0 3767   class class class wbr 4433   ` cfv 5574
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-nul 4562  ax-pow 4611
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-op 4017  df-uni 4231  df-br 4434  df-iota 5537  df-fv 5582
This theorem is referenced by:  dffv3  5848  fvrn0  5874  ndmfv  5876  csbfv  5890  dffv2  5927  fvmpti  5936  fvmptnf  5954  fvunsn  6084  1stval  6783  2ndval  6784  fipwuni  7884  fipwss  7887  tctr  8169  ranklim  8260  rankuni  8279  alephsing  8654  itunisuc  8797  itunitc1  8798  itunitc  8799  tskmcl  9217  hashfn  12417  strfvss  14522  strfvi  14544  setsnid  14546  elbasfv  14551  ressbas  14559  resslem  14562  firest  14702  topnval  14704  homffval  14958  comfffval  14965  oppchomfval  14981  oppcbas  14985  xpcbas  15316  lubfun  15479  glbfun  15492  oduval  15629  oduleval  15630  odumeet  15639  odujoin  15641  oduclatb  15643  ipopos  15659  isipodrs  15660  plusffval  15746  grpidval  15756  gsum0  15774  ismnd  15792  ismndOLD  15795  frmdplusg  15891  frmd0  15897  grpinvfval  15957  grpinvfvi  15960  grpsubfval  15961  mulgfval  16012  mulgfvi  16015  cntrval  16226  cntzval  16228  cntzrcl  16234  oppgval  16251  oppgplusfval  16252  symgbas  16274  symgplusg  16283  lactghmga  16298  pmtrfrn  16352  psgnfval  16394  odfval  16426  oppglsm  16531  efgval  16604  mgpval  17012  mgpplusg  17013  ringidval  17023  opprval  17141  opprmulfval  17142  dvdsrval  17162  invrfval  17190  dvrfval  17201  staffval  17364  scaffval  17398  islss  17449  sralem  17691  srasca  17695  sravsca  17696  sraip  17697  rlmval  17705  rlmsca2  17715  2idlval  17749  rrgval  17803  asclfval  17851  psrbas  17898  psrbasOLD  17899  psr1val  18093  vr1val  18099  ply1val  18101  ply1basfvi  18150  ply1plusgfvi  18151  psr1sca2  18160  ply1sca2  18163  ply1ascl  18167  evl1fval  18232  evl1fval1  18235  zrhval  18412  zlmlem  18421  zlmvsca  18426  chrval  18429  evpmss  18489  ipffval  18550  ocvval  18565  elocv  18566  thlbas  18594  thlle  18595  thloc  18597  pjfval  18604  istps  19304  tgdif0  19360  indislem  19367  txindislem  20000  fsubbas  20234  filuni  20252  ussval  20628  isusp  20630  nmfval  20975  tnglem  21020  tngds  21028  tchval  21527  deg1fval  22346  deg1fvi  22351  uc1pval  22406  mon1pval  22408  ttglem  24044  vafval  25361  bafval  25362  smfval  25363  vsfval  25393  resvsca  27686  resvlem  27687  mvtval  28726  mexval  28728  mexval2  28729  mdvval  28730  mrsubfval  28734  mrsubrn  28739  mrsub0  28742  mrsubf  28743  mrsubccat  28744  mrsubcn  28745  mrsubco  28747  mrsubvrs  28748  msubfval  28750  elmsubrn  28754  msubrn  28755  msubf  28758  mvhfval  28759  mpstval  28761  msrfval  28763  mstaval  28770  mclsrcl  28787  mppsval  28798  mthmval  28801  sltval2  29384  sltintdifex  29391  fvsingle  29538  funpartfv  29563  fullfunfv  29565  rankeq1o  29796  mzpmfp  30647  mzpmfpOLD  30648  kelac1  30977  mendbas  31102  mendplusgfval  31103  mendmulrfval  31105  mendsca  31107  mendvscafval  31108  atbase  34716  llnbase  34935  lplnbase  34960  lvolbase  35004  lhpbase  35424
  Copyright terms: Public domain W3C validator