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

Theorem fvprc 5859
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 5858 . 2  |-  ( -.  A  e.  _V  ->  -.  E! x  A F x )
2 tz6.12-2 5856 . 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 1444    e. wcel 1887   E!weu 2299   _Vcvv 3045   (/)c0 3731   class class class wbr 4402   ` cfv 5582
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-nul 4534  ax-pow 4581
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-br 4403  df-iota 5546  df-fv 5590
This theorem is referenced by:  dffv3  5861  fvrn0  5887  ndmfv  5889  csbfv  5902  dffv2  5938  fvmpti  5947  fvmptnf  5967  fvunsn  6096  brfvopab  6336  1stval  6795  2ndval  6796  fipwuni  7940  fipwss  7943  tctr  8224  ranklim  8315  rankuni  8334  alephsing  8706  itunisuc  8849  itunitc1  8850  itunitc  8851  tskmcl  9266  hashfn  12554  trclfvg  13079  trclfvcotrg  13080  strfvss  15139  strfvi  15163  setsnid  15165  elbasfv  15170  ressbas  15179  resslem  15182  firest  15331  topnval  15333  homffval  15595  comfffval  15603  oppchomfval  15619  oppcbas  15623  xpcbas  16063  lubfun  16226  glbfun  16239  oduval  16376  oduleval  16377  odumeet  16386  odujoin  16388  oduclatb  16390  ipopos  16406  isipodrs  16407  plusffval  16493  grpidval  16503  gsum0  16521  ismnd  16539  ismndOLD  16542  frmdplusg  16638  frmd0  16644  grpinvfval  16704  grpinvfvi  16707  grpsubfval  16708  mulgfval  16759  mulgfvi  16762  cntrval  16973  cntzval  16975  cntzrcl  16981  oppgval  16998  oppgplusfval  16999  symgbas  17021  symgplusg  17030  lactghmga  17045  pmtrfrn  17099  psgnfval  17141  odfval  17179  odfvalOLD  17182  oppglsm  17294  efgval  17367  mgpval  17726  mgpplusg  17727  ringidval  17737  opprval  17852  opprmulfval  17853  dvdsrval  17873  invrfval  17901  dvrfval  17912  staffval  18075  scaffval  18109  islss  18158  sralem  18400  srasca  18404  sravsca  18405  sraip  18406  rlmval  18414  rlmsca2  18424  2idlval  18457  rrgval  18511  asclfval  18558  psrbas  18602  psr1val  18779  vr1val  18785  ply1val  18787  ply1basfvi  18834  ply1plusgfvi  18835  psr1sca2  18844  ply1sca2  18847  ply1ascl  18851  evl1fval  18916  evl1fval1  18919  zrhval  19079  zlmlem  19088  zlmvsca  19093  chrval  19096  evpmss  19154  ipffval  19215  ocvval  19230  elocv  19231  thlbas  19259  thlle  19260  thloc  19262  pjfval  19269  istps  19951  tgdif0  20008  indislem  20015  txindislem  20648  fsubbas  20882  filuni  20900  ussval  21274  isusp  21276  nmfval  21603  tnglem  21648  tngds  21656  tchval  22192  deg1fval  23029  deg1fvi  23034  uc1pval  23090  mon1pval  23092  ttglem  24906  vafval  26222  bafval  26223  smfval  26224  vsfval  26254  resvsca  28593  resvlem  28594  mvtval  30138  mexval  30140  mexval2  30141  mdvval  30142  mrsubfval  30146  mrsubrn  30151  mrsub0  30154  mrsubf  30155  mrsubccat  30156  mrsubcn  30157  mrsubco  30159  mrsubvrs  30160  msubfval  30162  elmsubrn  30166  msubrn  30167  msubf  30170  mvhfval  30171  mpstval  30173  msrfval  30175  mstaval  30182  mclsrcl  30199  mppsval  30210  mthmval  30213  sltval2  30543  sltintdifex  30550  fvsingle  30687  funpartfv  30712  fullfunfv  30714  rankeq1o  30938  atbase  32855  llnbase  33074  lplnbase  33099  lvolbase  33143  lhpbase  33563  mzpmfp  35589  kelac1  35921  mendbas  36050  mendplusgfval  36051  mendmulrfval  36053  mendsca  36055  mendvscafval  36056  vtxvalprc  39145  iedgvalprc  39146  uvtxa0  39466  uvtxa01vtx  39470  wlkbProp  39632  rel1wlk  39640
  Copyright terms: Public domain W3C validator