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

Theorem fvprc 5680
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 5679 . 2  |-  ( -.  A  e.  _V  ->  -.  E! x  A F x )
2 tz6.12-2 5677 . 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 1369    e. wcel 1756   E!weu 2252   _Vcvv 2967   (/)c0 3632   class class class wbr 4287   ` cfv 5413
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-nul 4416  ax-pow 4465
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-iota 5376  df-fv 5421
This theorem is referenced by:  dffv3  5682  fvrn0  5707  ndmfv  5709  csbfv  5723  dffv2  5759  fvmpti  5768  fvmptnf  5786  fvunsn  5905  1stval  6574  2ndval  6575  fipwuni  7668  fipwss  7671  tctr  7952  ranklim  8043  rankuni  8062  alephsing  8437  itunisuc  8580  itunitc1  8581  itunitc  8582  tskmcl  9000  hashfn  12130  strfvss  14184  strfvi  14206  setsnid  14208  elbasfv  14213  ressbas  14220  resslem  14223  firest  14363  topnval  14365  homffval  14622  comfffval  14629  oppchomfval  14645  oppcbas  14649  xpcbas  14980  lubfun  15142  glbfun  15155  oduval  15292  oduleval  15293  odumeet  15302  odujoin  15304  oduclatb  15306  ipopos  15322  isipodrs  15323  ismnd  15409  plusffval  15419  grpidval  15424  gsum0  15501  frmdplusg  15523  frmd0  15529  grpinvfval  15567  grpinvfvi  15570  grpsubfval  15571  mulgfval  15619  mulgfvi  15622  cntrval  15828  cntzval  15830  cntzrcl  15836  oppgval  15853  oppgplusfval  15854  symgbas  15876  symgplusg  15885  lactghmga  15900  pmtrfrn  15955  psgnfval  15997  odfval  16027  oppglsm  16132  efgval  16205  mgpval  16584  mgpplusg  16585  rngidval  16595  opprval  16706  opprmulfval  16707  dvdsrval  16727  invrfval  16755  dvrfval  16766  staffval  16912  scaffval  16946  islss  16996  sralem  17238  srasca  17242  sravsca  17243  sraip  17244  rlmval  17252  rlmsca2  17262  2idlval  17295  rrgval  17338  asclfval  17385  psrbas  17428  psrbasOLD  17429  psr1val  17622  vr1val  17628  ply1val  17630  ply1basfvi  17676  ply1plusgfvi  17677  psr1sca2  17686  ply1sca2  17689  ply1ascl  17692  evl1fval  17742  evl1fval1  17745  zrhval  17919  zlmlem  17928  zlmvsca  17933  chrval  17936  evpmss  17996  ipffval  18057  ocvval  18072  elocv  18073  thlbas  18101  thlle  18102  thloc  18104  pjfval  18111  istps  18521  tgdif0  18577  indislem  18584  txindislem  19186  fsubbas  19420  filuni  19438  ussval  19814  isusp  19816  nmfval  20161  tnglem  20206  tngds  20214  tchval  20713  deg1fval  21531  deg1fvi  21536  uc1pval  21591  mon1pval  21593  ttglem  23094  vafval  23953  bafval  23954  smfval  23955  vsfval  23985  resvsca  26271  resvlem  26272  sltval2  27770  sltintdifex  27777  fvsingle  27924  funpartfv  27949  fullfunfv  27951  rankeq1o  28182  mzpmfp  29057  mzpmfpOLD  29058  kelac1  29390  mendbas  29515  mendplusgfval  29516  mendmulrfval  29518  mendsca  29520  mendvscafval  29521  atbase  32851  llnbase  33070  lplnbase  33095  lvolbase  33139  lhpbase  33559
  Copyright terms: Public domain W3C validator