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

Theorem fvprc 6642
Description: A function's value at a proper class is the empty set. (Contributed by NM, 20-May-1998.)
Assertion
Ref Expression
fvprc 𝐴 ∈ V → (𝐹𝐴) = ∅)

Proof of Theorem fvprc
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 brprcneu 6641 . 2 𝐴 ∈ V → ¬ ∃!𝑥 𝐴𝐹𝑥)
2 tz6.12-2 6639 . 2 (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹𝐴) = ∅)
31, 2syl 17 1 𝐴 ∈ V → (𝐹𝐴) = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1538  wcel 2112  ∃!weu 2631  Vcvv 3444  c0 4246   class class class wbr 5033  cfv 6328
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-nul 5177  ax-pow 5234
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-rex 3115  df-v 3446  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-iota 6287  df-fv 6336
This theorem is referenced by:  rnfvprc  6643  dffv3  6645  fvrn0  6677  ndmfv  6679  fv2prc  6689  csbfv  6694  dffv2  6737  brfvopabrbr  6746  fvmpti  6748  fvmptnf  6771  fvmptrabfv  6780  fvunsn  6922  fvmptopab  7192  brfvopab  7194  1stval  7677  2ndval  7678  fipwuni  8878  fipwss  8881  tctr  9170  ranklim  9261  rankuni  9280  alephsing  9691  itunisuc  9834  itunitc  9836  tskmcl  10256  hashfn  13736  s1prc  13953  trclfvg  14370  trclfvcotrg  14371  dfrtrclrec2  14413  rtrclreclem4  14416  dfrtrcl2  14417  strfvss  16502  strfvi  16533  setsnid  16535  elbasfv  16540  ressbas  16550  resslem  16553  firest  16702  topnval  16704  homffval  16956  comfffval  16964  oppchomfval  16980  oppcbas  16984  xpcbas  17424  lubfun  17586  glbfun  17599  oduval  17736  oduleval  17737  odumeet  17746  odujoin  17748  oduclatb  17750  ipopos  17766  isipodrs  17767  plusffval  17854  grpidval  17867  gsum0  17890  ismnd  17910  frmdplusg  18015  frmd0  18021  efmndbas  18032  efmndbasabf  18033  efmndplusg  18041  dfgrp2e  18125  grpinvfval  18138  grpinvfvalALT  18139  grpinvfvi  18142  grpsubfval  18143  grpsubfvalALT  18144  mulgfval  18222  mulgfvalALT  18223  mulgfvi  18226  cntrval  18445  cntzval  18447  cntzrcl  18453  oppgval  18471  oppgplusfval  18472  symgval  18493  symgplusg  18507  lactghmga  18529  psgnfval  18624  odfval  18656  odfvalALT  18657  oppglsm  18763  efgval  18839  mgpval  19239  mgpplusg  19240  ringidval  19250  opprval  19374  opprmulfval  19375  dvdsrval  19395  invrfval  19423  dvrfval  19434  staffval  19615  scaffval  19649  islss  19703  sralem  19946  sravsca  19951  sraip  19952  rlmval  19960  rlmsca2  19970  2idlval  20003  rrgval  20057  zrhval  20205  zlmlem  20214  zlmvsca  20219  chrval  20221  evpmss  20279  ipffval  20341  ocvval  20360  elocv  20361  thlbas  20389  thlle  20390  thloc  20392  pjfval  20399  asclfval  20569  psrbas  20620  psr1val  20819  vr1val  20825  ply1val  20827  ply1basfvi  20874  ply1plusgfvi  20875  psr1sca2  20884  ply1sca2  20887  ply1ascl  20891  evl1fval  20956  evl1fval1  20959  toponsspwpw  21531  istps  21543  tgdif0  21601  indislem  21609  txindislem  22242  fsubbas  22476  filuni  22494  ussval  22869  isusp  22871  nmfval  23199  tnglem  23250  tngds  23258  tcphval  23826  deg1fval  24685  deg1fvi  24690  uc1pval  24744  mon1pval  24746  ttglem  26674  vtxval  26797  iedgval  26798  vtxvalprc  26842  iedgvalprc  26843  edgval  26846  prcliscplgr  27208  wwlks  27625  wwlksn  27627  clwwlk  27772  clwwlkn  27815  clwwlknonmpo  27878  vafval  28390  bafval  28391  smfval  28392  vsfval  28420  resvsca  30958  resvlem  30959  prclisacycgr  32512  mvtval  32861  mexval  32863  mexval2  32864  mdvval  32865  mrsubfval  32869  msubfval  32885  elmsubrn  32889  mvhfval  32894  mpstval  32896  msrfval  32898  mstaval  32905  mclsrcl  32922  mppsval  32933  mthmval  32936  sltval2  33277  sltintdifex  33282  fvsingle  33495  funpartfv  33520  fullfunfv  33522  rankeq1o  33746  atbase  36584  llnbase  36804  lplnbase  36829  lvolbase  36873  lhpbase  37293  mzpmfp  39681  kelac1  40000  mendbas  40121  mendplusgfval  40122  mendmulrfval  40124  mendsca  40126  mendvscafval  40127  brfvimex  40722  clsneibex  40798  neicvgbex  40808  sprssspr  43991  sprsymrelfvlem  44000  prprelprb  44027  prprspr2  44028  upwlkbprop  44359
  Copyright terms: Public domain W3C validator