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

Theorem fvprc 6831
Description: A function's value at a proper class is the empty set. See fvprcALT 6832 for a proof that uses ax-pow 5318 instead of ax-pr 5382. (Contributed by NM, 20-May-1998.) Avoid ax-pow 5318. (Revised by BTernaryTau, 3-Aug-2024.) (Proof shortened by BTernaryTau, 3-Dec-2024.)
Assertion
Ref Expression
fvprc 𝐴 ∈ V → (𝐹𝐴) = ∅)

Proof of Theorem fvprc
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 brprcneu 6829 . 2 𝐴 ∈ V → ¬ ∃!𝑥 𝐴𝐹𝑥)
2 tz6.12-2 6827 . 2 (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹𝐴) = ∅)
31, 2syl 17 1 𝐴 ∈ V → (𝐹𝐴) = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1541  wcel 2106  ∃!weu 2566  Vcvv 3443  c0 4280   class class class wbr 5103  cfv 6493
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-nul 5261  ax-pr 5382
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3063  df-rex 3072  df-rab 3406  df-v 3445  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-br 5104  df-iota 6445  df-fv 6501
This theorem is referenced by:  rnfvprc  6833  dffv3  6835  fvrn0  6869  ndmfv  6874  fv2prc  6884  csbfv  6889  dffv2  6933  brfvopabrbr  6942  fvmpti  6944  fvmptnf  6967  fvmptrabfv  6976  fvunsn  7121  fvmptopab  7407  fvmptopabOLD  7408  brfvopab  7410  1stval  7919  2ndval  7920  fipwuni  9358  fipwss  9361  tctr  9672  ranklim  9776  rankuni  9795  alephsing  10208  itunisuc  10351  itunitc  10353  tskmcl  10773  hashfn  14267  s1prc  14484  trclfvg  14892  trclfvcotrg  14893  dfrtrclrec2  14935  rtrclreclem4  14938  dfrtrcl2  14939  strfvss  17051  strfvi  17054  fveqprc  17055  oveqprc  17056  setsnidOLD  17074  elbasfv  17081  ressbas  17110  ressbasOLD  17111  resslemOLD  17115  firest  17306  topnval  17308  homffval  17562  comfffval  17570  oppchomfval  17586  oppchomfvalOLD  17587  oppcbasOLD  17592  xpcbas  18058  oduval  18169  oduleval  18170  lubfun  18233  glbfun  18246  odujoin  18289  odumeet  18291  oduclatb  18388  ipopos  18417  isipodrs  18418  plusffval  18495  grpidval  18508  gsum0  18531  ismnd  18551  frmdplusg  18656  frmd0  18662  efmndbas  18673  efmndbasabf  18674  efmndplusg  18682  dfgrp2e  18768  grpinvfval  18781  grpinvfvalALT  18782  grpinvfvi  18785  grpsubfval  18786  grpsubfvalALT  18787  mulgfval  18865  mulgfvalALT  18866  mulgfvi  18869  cntrval  19090  cntzval  19092  cntzrcl  19098  oppgval  19116  oppgplusfval  19117  symgval  19141  lactghmga  19178  psgnfval  19273  odfval  19305  odfvalALT  19306  oppglsm  19415  efgval  19490  mgpval  19890  mgpplusg  19891  ringidval  19906  opprval  20035  opprmulfval  20036  dvdsrval  20059  invrfval  20087  dvrfval  20098  staffval  20291  scaffval  20325  islss  20380  sralem  20623  sralemOLD  20624  sravsca  20633  sravscaOLD  20634  sraip  20635  rlmval  20645  rlmsca2  20655  2idlval  20688  rrgval  20742  zrhval  20893  zlmlemOLD  20903  zlmvsca  20911  chrval  20913  evpmss  20975  ipffval  21037  ocvval  21056  elocv  21057  thlbas  21085  thlbasOLD  21086  thlle  21087  thlleOLD  21088  thloc  21090  pjfval  21097  asclfval  21267  psrbas  21331  psr1val  21541  vr1val  21547  ply1val  21549  ply1basfvi  21596  ply1plusgfvi  21597  psr1sca2  21606  ply1sca2  21609  ply1ascl  21613  evl1fval  21678  evl1fval1  21681  toponsspwpw  22255  istps  22267  tgdif0  22326  indislem  22334  txindislem  22968  fsubbas  23202  filuni  23220  ussval  23595  isusp  23597  nmfval  23928  tnglemOLD  23981  tngds  23995  tngdsOLD  23996  tcphval  24566  deg1fval  25429  deg1fvi  25434  uc1pval  25488  mon1pval  25490  sltval2  26988  sltintdifex  26993  ttglemOLD  27706  vtxval  27837  iedgval  27838  vtxvalprc  27882  iedgvalprc  27883  edgval  27886  prcliscplgr  28248  wwlks  28666  wwlksn  28668  clwwlk  28813  clwwlkn  28856  clwwlknonmpo  28919  vafval  29431  bafval  29432  smfval  29433  vsfval  29461  resvsca  32004  resvlemOLD  32006  prclisacycgr  33614  mvtval  33963  mexval  33965  mexval2  33966  mdvval  33967  mrsubfval  33971  msubfval  33987  elmsubrn  33991  mvhfval  33996  mpstval  33998  msrfval  34000  mstaval  34007  mclsrcl  34024  mppsval  34035  mthmval  34038  fvsingle  34472  funpartfv  34497  fullfunfv  34499  rankeq1o  34723  atbase  37718  llnbase  37939  lplnbase  37964  lvolbase  38008  lhpbase  38428  mzpmfp  41008  kelac1  41328  mendbas  41449  mendplusgfval  41450  mendmulrfval  41452  mendvscafval  41455  brfvimex  42240  clsneibex  42316  neicvgbex  42326  sprssspr  45605  sprsymrelfvlem  45614  prprelprb  45641  prprspr2  45642  upwlkbprop  45972  ipolub00  46950
  Copyright terms: Public domain W3C validator