![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fvprc | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
fvprc | ⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | brprcneu 6829 | . 2 ⊢ (¬ 𝐴 ∈ V → ¬ ∃!𝑥 𝐴𝐹𝑥) | |
2 | tz6.12-2 6827 | . 2 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅) | |
3 | 1, 2 | syl 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 |