![]() |
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 6894 for a proof that uses ax-pow 5369 instead of ax-pr 5433. (Contributed by NM, 20-May-1998.) Avoid ax-pow 5369. (Revised by BTernaryTau, 3-Aug-2024.) (Proof shortened by BTernaryTau, 3-Dec-2024.) |
Ref | Expression |
---|---|
fvprc | ⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | brprcneu 6891 | . 2 ⊢ (¬ 𝐴 ∈ V → ¬ ∃!𝑥 𝐴𝐹𝑥) | |
2 | tz6.12-2 6889 | . 2 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅) | |
3 | 1, 2 | syl 17 | 1 ⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1534 ∈ wcel 2099 ∃!weu 2557 Vcvv 3462 ∅c0 4325 class class class wbr 5153 ‘cfv 6554 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-nul 5311 ax-pr 5433 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2704 df-cleq 2718 df-clel 2803 df-ral 3052 df-rex 3061 df-rab 3420 df-v 3464 df-dif 3950 df-un 3952 df-ss 3964 df-nul 4326 df-if 4534 df-sn 4634 df-pr 4636 df-op 4640 df-uni 4914 df-br 5154 df-iota 6506 df-fv 6562 |
This theorem is referenced by: rnfvprc 6895 dffv3 6897 fvrn0 6931 ndmfv 6936 fv2prc 6946 csbfv 6951 dffv2 6997 brfvopabrbr 7006 fvmpti 7008 fvmptnf 7031 fvmptrabfv 7041 fvunsn 7193 fvmptopab 7479 fvmptopabOLD 7480 brfvopab 7482 1stval 8005 2ndval 8006 fipwuni 9469 fipwss 9472 tctr 9783 ranklim 9887 rankuni 9906 alephsing 10319 itunisuc 10462 itunitc 10464 tskmcl 10884 hashfn 14392 s1prc 14612 trclfvg 15020 trclfvcotrg 15021 dfrtrclrec2 15063 rtrclreclem4 15066 dfrtrcl2 15067 strfvss 17189 strfvi 17192 fveqprc 17193 oveqprc 17194 setsnidOLD 17212 elbasfv 17219 ressbas 17248 ressbasOLD 17249 resslemOLD 17256 firest 17447 topnval 17449 homffval 17703 comfffval 17711 oppchomfval 17727 oppchomfvalOLD 17728 oppcbasOLD 17733 xpcbas 18202 oduval 18313 oduleval 18314 lubfun 18377 glbfun 18390 odujoin 18433 odumeet 18435 oduclatb 18532 ipopos 18561 isipodrs 18562 plusffval 18639 grpidval 18654 gsum0 18677 ismnd 18730 frmdplusg 18844 frmd0 18850 efmndbas 18861 efmndbasabf 18862 efmndplusg 18870 dfgrp2e 18958 grpinvfval 18973 grpinvfvalALT 18974 grpinvfvi 18977 grpsubfval 18978 grpsubfvalALT 18979 mulgfval 19063 mulgfvalALT 19064 mulgfvi 19067 cntrval 19313 cntzval 19315 cntzrcl 19321 oppgval 19341 oppgplusfval 19342 symgval 19366 lactghmga 19403 psgnfval 19498 odfval 19530 odfvalALT 19531 oppglsm 19640 efgval 19715 mgpval 20120 mgpplusg 20121 ringidval 20166 opprval 20317 opprmulfval 20318 dvdsrval 20343 invrfval 20371 dvrfval 20384 rrgval 20675 staffval 20820 scaffval 20856 islss 20911 sralem 21154 sralemOLD 21155 sravsca 21164 sravscaOLD 21165 sraip 21166 rlmval 21177 rlmsca2 21185 2idlval 21240 zrhval 21497 zlmlemOLD 21507 zlmvsca 21515 chrval 21517 evpmss 21582 ipffval 21644 ocvval 21663 elocv 21664 thlbas 21692 thlbasOLD 21693 thlle 21694 thlleOLD 21695 thloc 21697 pjfval 21704 asclfval 21876 psrbas 21942 psr1val 22175 vr1val 22181 ply1val 22183 ply1basfvi 22230 ply1plusgfvi 22231 psr1sca2 22240 ply1sca2 22243 ply1ascl 22249 evl1fval 22319 evl1fval1 22322 toponsspwpw 22915 istps 22927 tgdif0 22986 indislem 22994 txindislem 23628 fsubbas 23862 filuni 23880 ussval 24255 isusp 24257 nmfval 24588 tnglemOLD 24641 tngds 24655 tngdsOLD 24656 tcphval 25237 deg1fval 26107 deg1fvi 26112 uc1pval 26167 mon1pval 26169 sltval2 27686 sltintdifex 27691 ttglemOLD 28805 vtxval 28936 iedgval 28937 vtxvalprc 28981 iedgvalprc 28982 edgval 28985 prcliscplgr 29350 wwlks 29769 wwlksn 29771 clwwlk 29916 clwwlkn 29959 clwwlknonmpo 30022 vafval 30536 bafval 30537 smfval 30538 vsfval 30566 erlval 33113 fracval 33154 fracbas 33155 resvsca 33204 resvlemOLD 33206 prclisacycgr 34979 mvtval 35328 mexval 35330 mexval2 35331 mdvval 35332 mrsubfval 35336 msubfval 35352 elmsubrn 35356 mvhfval 35361 mpstval 35363 msrfval 35365 mstaval 35372 mclsrcl 35389 mppsval 35400 mthmval 35403 fvsingle 35744 funpartfv 35769 fullfunfv 35771 rankeq1o 35995 atbase 38987 llnbase 39208 lplnbase 39233 lvolbase 39277 lhpbase 39697 mzpmfp 42404 kelac1 42724 mendbas 42845 mendplusgfval 42846 mendmulrfval 42848 mendvscafval 42851 brfvimex 43693 clsneibex 43769 neicvgbex 43779 sprssspr 47053 sprsymrelfvlem 47062 prprelprb 47089 prprspr2 47090 upwlkbprop 47515 ipolub00 48319 |
Copyright terms: Public domain | W3C validator |