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

Theorem fvprc 5685
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 5684 . 2  |-  ( -.  A  e.  _V  ->  -.  E! x  A F x )
2 tz6.12-2 5682 . 2  |-  ( -.  E! x  A F x  ->  ( F `  A )  =  (/) )
31, 2syl 16 1  |-  ( -.  A  e.  _V  ->  ( F `  A )  =  (/) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1649    e. wcel 1721   E!weu 2258   _Vcvv 2920   (/)c0 3592   class class class wbr 4176   ` cfv 5417
This theorem is referenced by:  dffv3  5687  fvrn0  5716  ndmfv  5718  dffv2  5759  fvmpti  5768  fvmptnf  5785  fvunsn  5888  1stval  6314  2ndval  6315  riotav  6517  riotaprc  6550  riotassuni  6551  fipwuni  7393  fipwss  7396  tctr  7639  ranklim  7730  rankuni  7749  alephsing  8116  itunisuc  8259  itunitc1  8260  itunitc  8261  tskmcl  8676  hashfn  11608  strfvss  13446  strfvi  13466  setsnid  13468  elbasfv  13471  ressbas  13478  resslem  13481  firest  13619  topnval  13621  homffval  13876  comfffval  13883  oppchomfval  13899  oppcbas  13903  xpcbas  14234  oduval  14516  oduleval  14517  odumeet  14526  odujoin  14528  oduclatb  14530  ipopos  14545  isipodrs  14546  ismnd  14651  plusffval  14661  grpidval  14666  gsum0  14739  frmdplusg  14758  frmd0  14764  grpinvfval  14802  grpinvfvi  14805  grpsubfval  14806  mulgfval  14850  mulgfvi  14853  symgbas  15054  symgplusg  15058  lactghmga  15066  cntrval  15077  cntzval  15079  cntzrcl  15085  oppgval  15102  oppgplusfval  15103  odfval  15130  oppglsm  15235  efgval  15308  mgpval  15610  mgpplusg  15611  rngidval  15625  opprval  15688  opprmulfval  15689  dvdsrval  15709  invrfval  15737  dvrfval  15748  staffval  15894  scaffval  15927  islss  15970  sralem  16208  srasca  16212  sravsca  16213  rlmval  16223  rlmsca2  16231  2idlval  16263  rrgval  16306  asclfval  16352  psrbas  16402  psr1val  16543  vr1val  16549  ply1val  16551  ply1basfvi  16594  ply1plusgfvi  16595  psr1sca2  16604  ply1sca2  16607  ply1ascl  16610  zrhval  16748  zlmlem  16757  zlmvsca  16762  chrval  16765  ipffval  16838  ocvval  16853  elocv  16854  thlbas  16882  thlle  16883  thloc  16885  pjfval  16892  istps  16960  tgdif0  17016  indislem  17023  txindislem  17622  fsubbas  17856  filuni  17874  ussval  18246  isusp  18248  nmfval  18593  tnglem  18638  tngds  18646  tchval  19134  evl1fval  19904  deg1fval  19960  deg1fvi  19965  uc1pval  20019  mon1pval  20021  vafval  22039  bafval  22040  smfval  22041  vsfval  22071  sltval2  25528  sltintdifex  25535  funpartfv  25702  fullfunfv  25704  rankeq1o  26020  mzpmfp  26698  kelac1  27033  pmtrfrn  27272  psgnfval  27295  mendbas  27364  mendplusgfval  27365  mendmulrfval  27367  mendsca  27369  mendvscafval  27370  atbase  29776  llnbase  29995  lplnbase  30020  lvolbase  30064  lhpbase  30484
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-nul 4302  ax-pow 4341
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2262  df-mo 2263  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-ral 2675  df-rex 2676  df-rab 2679  df-v 2922  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-nul 3593  df-if 3704  df-sn 3784  df-pr 3785  df-op 3787  df-uni 3980  df-br 4177  df-iota 5381  df-fv 5425
  Copyright terms: Public domain W3C validator