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

Theorem fvprc 5873
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 5872 . 2  |-  ( -.  A  e.  _V  ->  -.  E! x  A F x )
2 tz6.12-2 5870 . 2  |-  ( -.  E! x  A F x  ->  ( F `  A )  =  (/) )
31, 2syl 17 1  |-  ( -.  A  e.  _V  ->  ( F `  A )  =  (/) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1452    e. wcel 1904   E!weu 2319   _Vcvv 3031   (/)c0 3722   class class class wbr 4395   ` cfv 5589
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-nul 4527  ax-pow 4579
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-br 4396  df-iota 5553  df-fv 5597
This theorem is referenced by:  dffv3  5875  fvrn0  5901  ndmfv  5903  csbfv  5916  dffv2  5953  fvmpti  5962  fvmptnf  5982  fvunsn  6112  brfvopab  6355  1stval  6814  2ndval  6815  fipwuni  7958  fipwss  7961  tctr  8242  ranklim  8333  rankuni  8352  alephsing  8724  itunisuc  8867  itunitc1  8868  itunitc  8869  tskmcl  9284  hashfn  12592  trclfvg  13156  trclfvcotrg  13157  strfvss  15217  strfvi  15241  setsnid  15243  elbasfv  15248  ressbas  15257  resslem  15260  firest  15409  topnval  15411  homffval  15673  comfffval  15681  oppchomfval  15697  oppcbas  15701  xpcbas  16141  lubfun  16304  glbfun  16317  oduval  16454  oduleval  16455  odumeet  16464  odujoin  16466  oduclatb  16468  ipopos  16484  isipodrs  16485  plusffval  16571  grpidval  16581  gsum0  16599  ismnd  16617  ismndOLD  16620  frmdplusg  16716  frmd0  16722  grpinvfval  16782  grpinvfvi  16785  grpsubfval  16786  mulgfval  16837  mulgfvi  16840  cntrval  17051  cntzval  17053  cntzrcl  17059  oppgval  17076  oppgplusfval  17077  symgbas  17099  symgplusg  17108  lactghmga  17123  pmtrfrn  17177  psgnfval  17219  odfval  17257  odfvalOLD  17260  oppglsm  17372  efgval  17445  mgpval  17804  mgpplusg  17805  ringidval  17815  opprval  17930  opprmulfval  17931  dvdsrval  17951  invrfval  17979  dvrfval  17990  staffval  18153  scaffval  18187  islss  18236  sralem  18478  srasca  18482  sravsca  18483  sraip  18484  rlmval  18492  rlmsca2  18502  2idlval  18534  rrgval  18588  asclfval  18635  psrbas  18679  psr1val  18856  vr1val  18862  ply1val  18864  ply1basfvi  18911  ply1plusgfvi  18912  psr1sca2  18921  ply1sca2  18924  ply1ascl  18928  evl1fval  18993  evl1fval1  18996  zrhval  19156  zlmlem  19165  zlmvsca  19170  chrval  19173  evpmss  19231  ipffval  19292  ocvval  19307  elocv  19308  thlbas  19336  thlle  19337  thloc  19339  pjfval  19346  istps  20028  tgdif0  20085  indislem  20092  txindislem  20725  fsubbas  20960  filuni  20978  ussval  21352  isusp  21354  nmfval  21681  tnglem  21726  tngds  21734  tchval  22270  deg1fval  23108  deg1fvi  23113  uc1pval  23169  mon1pval  23171  ttglem  24985  vafval  26303  bafval  26304  smfval  26305  vsfval  26335  resvsca  28667  resvlem  28668  mvtval  30210  mexval  30212  mexval2  30213  mdvval  30214  mrsubfval  30218  mrsubrn  30223  mrsub0  30226  mrsubf  30227  mrsubccat  30228  mrsubcn  30229  mrsubco  30231  mrsubvrs  30232  msubfval  30234  elmsubrn  30238  msubrn  30239  msubf  30242  mvhfval  30243  mpstval  30245  msrfval  30247  mstaval  30254  mclsrcl  30271  mppsval  30282  mthmval  30285  sltval2  30614  sltintdifex  30621  fvsingle  30758  funpartfv  30783  fullfunfv  30785  rankeq1o  31009  atbase  32926  llnbase  33145  lplnbase  33170  lvolbase  33214  lhpbase  33634  mzpmfp  35660  kelac1  35992  mendbas  36121  mendplusgfval  36122  mendmulrfval  36124  mendsca  36126  mendvscafval  36127  vtxvalprc  39298  iedgvalprc  39299  uvtxa0  39630  uvtxa01vtx  39634  wlkbProp  39819
  Copyright terms: Public domain W3C validator