![]() |
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 6835 for a proof that uses ax-pow 5320 instead of ax-pr 5384. (Contributed by NM, 20-May-1998.) Avoid ax-pow 5320. (Revised by BTernaryTau, 3-Aug-2024.) (Proof shortened by BTernaryTau, 3-Dec-2024.) |
Ref | Expression |
---|---|
fvprc | ⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | brprcneu 6832 | . 2 ⊢ (¬ 𝐴 ∈ V → ¬ ∃!𝑥 𝐴𝐹𝑥) | |
2 | tz6.12-2 6830 | . 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 3445 ∅c0 4282 class class class wbr 5105 ‘cfv 6496 |
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 5263 ax-pr 5384 |
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 3065 df-rex 3074 df-rab 3408 df-v 3447 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-nul 4283 df-if 4487 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-br 5106 df-iota 6448 df-fv 6504 |
This theorem is referenced by: rnfvprc 6836 dffv3 6838 fvrn0 6872 ndmfv 6877 fv2prc 6887 csbfv 6892 dffv2 6936 brfvopabrbr 6945 fvmpti 6947 fvmptnf 6970 fvmptrabfv 6979 fvunsn 7125 fvmptopab 7411 fvmptopabOLD 7412 brfvopab 7414 1stval 7923 2ndval 7924 fipwuni 9362 fipwss 9365 tctr 9676 ranklim 9780 rankuni 9799 alephsing 10212 itunisuc 10355 itunitc 10357 tskmcl 10777 hashfn 14275 s1prc 14492 trclfvg 14900 trclfvcotrg 14901 dfrtrclrec2 14943 rtrclreclem4 14946 dfrtrcl2 14947 strfvss 17059 strfvi 17062 fveqprc 17063 oveqprc 17064 setsnidOLD 17082 elbasfv 17089 ressbas 17118 ressbasOLD 17119 resslemOLD 17123 firest 17314 topnval 17316 homffval 17570 comfffval 17578 oppchomfval 17594 oppchomfvalOLD 17595 oppcbasOLD 17600 xpcbas 18066 oduval 18177 oduleval 18178 lubfun 18241 glbfun 18254 odujoin 18297 odumeet 18299 oduclatb 18396 ipopos 18425 isipodrs 18426 plusffval 18503 grpidval 18516 gsum0 18539 ismnd 18559 frmdplusg 18664 frmd0 18670 efmndbas 18681 efmndbasabf 18682 efmndplusg 18690 dfgrp2e 18776 grpinvfval 18789 grpinvfvalALT 18790 grpinvfvi 18793 grpsubfval 18794 grpsubfvalALT 18795 mulgfval 18874 mulgfvalALT 18875 mulgfvi 18878 cntrval 19099 cntzval 19101 cntzrcl 19107 oppgval 19125 oppgplusfval 19126 symgval 19150 lactghmga 19187 psgnfval 19282 odfval 19314 odfvalALT 19315 oppglsm 19424 efgval 19499 mgpval 19899 mgpplusg 19900 ringidval 19915 opprval 20050 opprmulfval 20051 dvdsrval 20074 invrfval 20102 dvrfval 20113 staffval 20306 scaffval 20340 islss 20395 sralem 20638 sralemOLD 20639 sravsca 20648 sravscaOLD 20649 sraip 20650 rlmval 20660 rlmsca2 20670 2idlval 20703 rrgval 20757 zrhval 20908 zlmlemOLD 20918 zlmvsca 20926 chrval 20928 evpmss 20990 ipffval 21052 ocvval 21071 elocv 21072 thlbas 21100 thlbasOLD 21101 thlle 21102 thlleOLD 21103 thloc 21105 pjfval 21112 asclfval 21282 psrbas 21346 psr1val 21557 vr1val 21563 ply1val 21565 ply1basfvi 21612 ply1plusgfvi 21613 psr1sca2 21622 ply1sca2 21625 ply1ascl 21629 evl1fval 21694 evl1fval1 21697 toponsspwpw 22271 istps 22283 tgdif0 22342 indislem 22350 txindislem 22984 fsubbas 23218 filuni 23236 ussval 23611 isusp 23613 nmfval 23944 tnglemOLD 23997 tngds 24011 tngdsOLD 24012 tcphval 24582 deg1fval 25445 deg1fvi 25450 uc1pval 25504 mon1pval 25506 sltval2 27004 sltintdifex 27009 ttglemOLD 27820 vtxval 27951 iedgval 27952 vtxvalprc 27996 iedgvalprc 27997 edgval 28000 prcliscplgr 28362 wwlks 28780 wwlksn 28782 clwwlk 28927 clwwlkn 28970 clwwlknonmpo 29033 vafval 29545 bafval 29546 smfval 29547 vsfval 29575 resvsca 32121 resvlemOLD 32123 prclisacycgr 33745 mvtval 34094 mexval 34096 mexval2 34097 mdvval 34098 mrsubfval 34102 msubfval 34118 elmsubrn 34122 mvhfval 34127 mpstval 34129 msrfval 34131 mstaval 34138 mclsrcl 34155 mppsval 34166 mthmval 34169 fvsingle 34505 funpartfv 34530 fullfunfv 34532 rankeq1o 34756 atbase 37751 llnbase 37972 lplnbase 37997 lvolbase 38041 lhpbase 38461 mzpmfp 41056 kelac1 41376 mendbas 41497 mendplusgfval 41498 mendmulrfval 41500 mendvscafval 41503 brfvimex 42288 clsneibex 42364 neicvgbex 42374 sprssspr 45663 sprsymrelfvlem 45672 prprelprb 45699 prprspr2 45700 upwlkbprop 46030 ipolub00 47008 |
Copyright terms: Public domain | W3C validator |