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

Theorem fvprc 6531
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 6530 . 2 𝐴 ∈ V → ¬ ∃!𝑥 𝐴𝐹𝑥)
2 tz6.12-2 6528 . 2 (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹𝐴) = ∅)
31, 2syl 17 1 𝐴 ∈ V → (𝐹𝐴) = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1522  wcel 2081  ∃!weu 2611  Vcvv 3437  c0 4211   class class class wbr 4962  cfv 6225
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769  ax-nul 5101  ax-pow 5157
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-sn 4473  df-pr 4475  df-op 4479  df-uni 4746  df-br 4963  df-iota 6189  df-fv 6233
This theorem is referenced by:  rnfvprc  6532  dffv3  6534  fvrn0  6566  ndmfv  6568  fv2prc  6578  csbfv  6583  dffv2  6623  brfvopabrbr  6632  fvmpti  6634  fvmptnf  6656  fvmptrabfv  6664  fvunsn  6804  fvmptopab  7068  brfvopab  7070  1stval  7547  2ndval  7548  fipwuni  8736  fipwss  8739  tctr  9028  ranklim  9119  rankuni  9138  alephsing  9544  itunisuc  9687  itunitc  9689  tskmcl  10109  hashfn  13584  s1prc  13802  trclfvg  14209  trclfvcotrg  14210  strfvss  16335  strfvi  16366  setsnid  16368  elbasfv  16373  ressbas  16383  resslem  16386  firest  16535  topnval  16537  homffval  16789  comfffval  16797  oppchomfval  16813  oppcbas  16817  xpcbas  17257  lubfun  17419  glbfun  17432  oduval  17569  oduleval  17570  odumeet  17579  odujoin  17581  oduclatb  17583  ipopos  17599  isipodrs  17600  plusffval  17686  grpidval  17699  gsum0  17717  ismnd  17736  frmdplusg  17830  frmd0  17836  dfgrp2e  17887  grpinvfval  17899  grpinvfvalALT  17900  grpinvfvi  17903  grpsubfval  17904  grpsubfvalALT  17905  mulgfval  17983  mulgfvalALT  17984  mulgfvi  17987  cntrval  18190  cntzval  18192  cntzrcl  18198  oppgval  18216  oppgplusfval  18217  symgbas  18239  symgplusg  18248  lactghmga  18263  psgnfval  18359  odfval  18391  odfvalALT  18392  oppglsm  18497  efgval  18570  mgpval  18932  mgpplusg  18933  ringidval  18943  opprval  19064  opprmulfval  19065  dvdsrval  19085  invrfval  19113  dvrfval  19124  staffval  19308  scaffval  19342  islss  19396  sralem  19639  sravsca  19644  sraip  19645  rlmval  19653  rlmsca2  19663  2idlval  19695  rrgval  19749  asclfval  19796  psrbas  19846  psr1val  20037  vr1val  20043  ply1val  20045  ply1basfvi  20092  ply1plusgfvi  20093  psr1sca2  20102  ply1sca2  20105  ply1ascl  20109  evl1fval  20173  evl1fval1  20176  zrhval  20337  zlmlem  20346  zlmvsca  20351  chrval  20354  evpmss  20412  ipffval  20474  ocvval  20493  elocv  20494  thlbas  20522  thlle  20523  thloc  20525  pjfval  20532  toponsspwpw  21214  istps  21226  tgdif0  21284  indislem  21292  txindislem  21925  fsubbas  22159  filuni  22177  ussval  22551  isusp  22553  nmfval  22881  tnglem  22932  tngds  22940  tcphval  23504  deg1fval  24357  deg1fvi  24362  uc1pval  24416  mon1pval  24418  ttglem  26345  vtxval  26468  iedgval  26469  vtxvalprc  26513  iedgvalprc  26514  edgval  26517  prcliscplgr  26879  wwlks  27300  wwlksn  27302  clwwlk  27448  clwwlkn  27491  clwwlknonmpo  27555  vafval  28071  bafval  28072  smfval  28073  vsfval  28101  resvsca  30557  resvlem  30558  prclisacycgr  32006  mvtval  32355  mexval  32357  mexval2  32358  mdvval  32359  mrsubfval  32363  msubfval  32379  elmsubrn  32383  mvhfval  32388  mpstval  32390  msrfval  32392  mstaval  32399  mclsrcl  32416  mppsval  32427  mthmval  32430  sltval2  32772  sltintdifex  32777  fvsingle  32990  funpartfv  33015  fullfunfv  33017  rankeq1o  33241  atbase  35956  llnbase  36176  lplnbase  36201  lvolbase  36245  lhpbase  36665  mzpmfp  38829  kelac1  39148  mendbas  39269  mendplusgfval  39270  mendmulrfval  39272  mendsca  39274  mendvscafval  39275  brfvimex  39861  clsneibex  39937  neicvgbex  39947  sprssspr  43125  sprsymrelfvlem  43134  prprelprb  43161  prprspr2  43162  upwlkbprop  43495
  Copyright terms: Public domain W3C validator