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

Theorem fvprc 5722
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 5721 . 2  |-  ( -.  A  e.  _V  ->  -.  E! x  A F x )
2 tz6.12-2 5719 . 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 1652    e. wcel 1725   E!weu 2281   _Vcvv 2956   (/)c0 3628   class class class wbr 4212   ` cfv 5454
This theorem is referenced by:  dffv3  5724  fvrn0  5753  ndmfv  5755  dffv2  5796  fvmpti  5805  fvmptnf  5822  fvunsn  5925  1stval  6351  2ndval  6352  riotav  6554  riotaprc  6587  riotassuni  6588  fipwuni  7431  fipwss  7434  tctr  7679  ranklim  7770  rankuni  7789  alephsing  8156  itunisuc  8299  itunitc1  8300  itunitc  8301  tskmcl  8716  hashfn  11649  strfvss  13487  strfvi  13507  setsnid  13509  elbasfv  13512  ressbas  13519  resslem  13522  firest  13660  topnval  13662  homffval  13917  comfffval  13924  oppchomfval  13940  oppcbas  13944  xpcbas  14275  oduval  14557  oduleval  14558  odumeet  14567  odujoin  14569  oduclatb  14571  ipopos  14586  isipodrs  14587  ismnd  14692  plusffval  14702  grpidval  14707  gsum0  14780  frmdplusg  14799  frmd0  14805  grpinvfval  14843  grpinvfvi  14846  grpsubfval  14847  mulgfval  14891  mulgfvi  14894  symgbas  15095  symgplusg  15099  lactghmga  15107  cntrval  15118  cntzval  15120  cntzrcl  15126  oppgval  15143  oppgplusfval  15144  odfval  15171  oppglsm  15276  efgval  15349  mgpval  15651  mgpplusg  15652  rngidval  15666  opprval  15729  opprmulfval  15730  dvdsrval  15750  invrfval  15778  dvrfval  15789  staffval  15935  scaffval  15968  islss  16011  sralem  16249  srasca  16253  sravsca  16254  rlmval  16264  rlmsca2  16272  2idlval  16304  rrgval  16347  asclfval  16393  psrbas  16443  psr1val  16584  vr1val  16590  ply1val  16592  ply1basfvi  16635  ply1plusgfvi  16636  psr1sca2  16645  ply1sca2  16648  ply1ascl  16651  zrhval  16789  zlmlem  16798  zlmvsca  16803  chrval  16806  ipffval  16879  ocvval  16894  elocv  16895  thlbas  16923  thlle  16924  thloc  16926  pjfval  16933  istps  17001  tgdif0  17057  indislem  17064  txindislem  17665  fsubbas  17899  filuni  17917  ussval  18289  isusp  18291  nmfval  18636  tnglem  18681  tngds  18689  tchval  19177  evl1fval  19947  deg1fval  20003  deg1fvi  20008  uc1pval  20062  mon1pval  20064  vafval  22082  bafval  22083  smfval  22084  vsfval  22114  sltval2  25611  sltintdifex  25618  fvsingle  25765  funpartfv  25790  fullfunfv  25792  rankeq1o  26112  mzpmfp  26804  kelac1  27138  pmtrfrn  27377  psgnfval  27400  mendbas  27469  mendplusgfval  27470  mendmulrfval  27472  mendsca  27474  mendvscafval  27475  atbase  30087  llnbase  30306  lplnbase  30331  lvolbase  30375  lhpbase  30795
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-nul 4338  ax-pow 4377
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-mo 2286  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2958  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-uni 4016  df-br 4213  df-iota 5418  df-fv 5462
  Copyright terms: Public domain W3C validator