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

Theorem fvprc 6144
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 6143 . 2 𝐴 ∈ V → ¬ ∃!𝑥 𝐴𝐹𝑥)
2 tz6.12-2 6141 . 2 (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹𝐴) = ∅)
31, 2syl 17 1 𝐴 ∈ V → (𝐹𝐴) = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1480  wcel 1992  ∃!weu 2474  Vcvv 3191  c0 3896   class class class wbr 4618  cfv 5850
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-nul 4754  ax-pow 4808
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3193  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-iota 5813  df-fv 5858
This theorem is referenced by:  dffv3  6146  fvrn0  6174  ndmfv  6176  fv2prc  6186  csbfv  6191  dffv2  6229  brfvopabrbr  6237  fvmpti  6239  fvmptnf  6259  fvunsn  6400  fvmptopab  6651  brfvopab  6654  1stval  7118  2ndval  7119  fipwuni  8277  fipwss  8280  tctr  8561  ranklim  8652  rankuni  8671  alephsing  9043  itunisuc  9186  itunitc1  9187  itunitc  9188  tskmcl  9608  hashfn  13101  trclfvg  13685  trclfvcotrg  13686  strfvss  15797  strfvi  15829  setsnid  15831  elbasfv  15836  ressbas  15846  resslem  15849  firest  16009  topnval  16011  homffval  16266  comfffval  16274  oppchomfval  16290  oppcbas  16294  xpcbas  16734  lubfun  16896  glbfun  16909  oduval  17046  oduleval  17047  odumeet  17056  odujoin  17058  oduclatb  17060  ipopos  17076  isipodrs  17077  plusffval  17163  grpidval  17176  gsum0  17194  ismnd  17213  frmdplusg  17307  frmd0  17313  dfgrp2e  17364  grpinvfval  17376  grpinvfvi  17379  grpsubfval  17380  mulgfval  17458  mulgfvi  17461  cntrval  17668  cntzval  17670  cntzrcl  17676  oppgval  17693  oppgplusfval  17694  symgbas  17716  symgplusg  17725  lactghmga  17740  pmtrfrn  17794  psgnfval  17836  odfval  17868  oppglsm  17973  efgval  18046  mgpval  18408  mgpplusg  18409  ringidval  18419  opprval  18540  opprmulfval  18541  dvdsrval  18561  invrfval  18589  dvrfval  18600  staffval  18763  scaffval  18797  islss  18849  sralem  19091  srasca  19095  sravsca  19096  sraip  19097  rlmval  19105  rlmsca2  19115  2idlval  19147  rrgval  19201  asclfval  19248  psrbas  19292  psr1val  19470  vr1val  19476  ply1val  19478  ply1basfvi  19525  ply1plusgfvi  19526  psr1sca2  19535  ply1sca2  19538  ply1ascl  19542  evl1fval  19606  evl1fval1  19609  zrhval  19770  zlmlem  19779  zlmvsca  19784  chrval  19787  evpmss  19846  ipffval  19907  ocvval  19925  elocv  19926  thlbas  19954  thlle  19955  thloc  19957  pjfval  19964  istps  20646  tgdif0  20702  indislem  20709  txindislem  21341  fsubbas  21576  filuni  21594  ussval  21968  isusp  21970  nmfval  22298  tnglem  22349  tngds  22357  tchval  22920  deg1fval  23739  deg1fvi  23744  uc1pval  23798  mon1pval  23800  ttglem  25651  vtxval  25773  iedgval  25774  vtxvalprc  25832  iedgvalprc  25833  uvtxa0  26175  uvtxa01vtx  26179  wwlks  26590  wwlksn  26592  clwwlks  26740  clwwlksn  26742  vafval  27298  bafval  27299  smfval  27300  vsfval  27328  resvsca  29607  resvlem  29608  mvtval  31097  mexval  31099  mexval2  31100  mdvval  31101  mrsubfval  31105  mrsubrn  31110  mrsub0  31113  mrsubf  31114  mrsubccat  31115  mrsubcn  31116  mrsubco  31118  mrsubvrs  31119  msubfval  31121  elmsubrn  31125  msubrn  31126  msubf  31129  mvhfval  31130  mpstval  31132  msrfval  31134  mstaval  31141  mclsrcl  31158  mppsval  31169  mthmval  31172  sltval2  31502  sltintdifex  31509  fvsingle  31661  funpartfv  31686  fullfunfv  31688  rankeq1o  31912  bj-toponss  32689  atbase  34042  llnbase  34261  lplnbase  34286  lvolbase  34330  lhpbase  34750  mzpmfp  36776  kelac1  37099  mendbas  37221  mendplusgfval  37222  mendmulrfval  37224  mendsca  37226  mendvscafval  37227  brfvimex  37792  clsneibex  37868  neicvgbex  37878  upwlkbprop  40995  sprssspr  41007  sprsymrelfvlem  41015
  Copyright terms: Public domain W3C validator