![]() |
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. (Contributed by NM, 20-May-1998.) |
Ref | Expression |
---|---|
fvprc | ⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | brprcneu 6325 | . 2 ⊢ (¬ 𝐴 ∈ V → ¬ ∃!𝑥 𝐴𝐹𝑥) | |
2 | tz6.12-2 6323 | . 2 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅) | |
3 | 1, 2 | syl 17 | 1 ⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1631 ∈ wcel 2145 ∃!weu 2618 Vcvv 3351 ∅c0 4063 class class class wbr 4786 ‘cfv 6031 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-8 2147 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-nul 4923 ax-pow 4974 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 835 df-3an 1073 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-eu 2622 df-mo 2623 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ral 3066 df-rex 3067 df-rab 3070 df-v 3353 df-dif 3726 df-un 3728 df-in 3730 df-ss 3737 df-nul 4064 df-if 4226 df-sn 4317 df-pr 4319 df-op 4323 df-uni 4575 df-br 4787 df-iota 5994 df-fv 6039 |
This theorem is referenced by: dffv3 6328 fvrn0 6357 ndmfv 6359 fv2prc 6369 csbfv 6374 dffv2 6413 brfvopabrbr 6421 fvmpti 6423 fvmptnf 6444 fvmptrabfv 6451 fvunsn 6589 fvmptopab 6844 brfvopab 6847 1stval 7317 2ndval 7318 fipwuni 8488 fipwss 8491 tctr 8780 ranklim 8871 rankuni 8890 alephsing 9300 itunisuc 9443 itunitc1 9444 itunitc 9445 tskmcl 9865 hashfn 13366 s1prc 13584 trclfvg 13964 trclfvcotrg 13965 strfvss 16087 strfvi 16120 setsnid 16122 elbasfv 16127 ressbas 16137 resslem 16140 firest 16301 topnval 16303 homffval 16557 comfffval 16565 oppchomfval 16581 oppcbas 16585 xpcbas 17026 lubfun 17188 glbfun 17201 oduval 17338 oduleval 17339 odumeet 17348 odujoin 17350 oduclatb 17352 ipopos 17368 isipodrs 17369 plusffval 17455 grpidval 17468 gsum0 17486 ismnd 17505 frmdplusg 17599 frmd0 17605 dfgrp2e 17656 grpinvfval 17668 grpinvfvi 17671 grpsubfval 17672 mulgfval 17750 mulgfvi 17753 cntrval 17959 cntzval 17961 cntzrcl 17967 oppgval 17984 oppgplusfval 17985 symgbas 18007 symgplusg 18016 lactghmga 18031 pmtrfrn 18085 psgnfval 18127 odfval 18159 oppglsm 18264 efgval 18337 mgpval 18700 mgpplusg 18701 ringidval 18711 opprval 18832 opprmulfval 18833 dvdsrval 18853 invrfval 18881 dvrfval 18892 staffval 19057 scaffval 19091 islss 19145 sralem 19392 srasca 19396 sravsca 19397 sraip 19398 rlmval 19406 rlmsca2 19416 2idlval 19448 rrgval 19502 asclfval 19549 psrbas 19593 psr1val 19771 vr1val 19777 ply1val 19779 ply1basfvi 19826 ply1plusgfvi 19827 psr1sca2 19836 ply1sca2 19839 ply1ascl 19843 evl1fval 19907 evl1fval1 19910 zrhval 20071 zlmlem 20080 zlmvsca 20085 chrval 20088 evpmss 20147 ipffval 20210 ocvval 20228 elocv 20229 thlbas 20257 thlle 20258 thloc 20260 pjfval 20267 toponsspwpw 20947 istps 20959 tgdif0 21017 indislem 21025 txindislem 21657 fsubbas 21891 filuni 21909 ussval 22283 isusp 22285 nmfval 22613 tnglem 22664 tngds 22672 tchval 23236 deg1fval 24060 deg1fvi 24065 uc1pval 24119 mon1pval 24121 ttglem 25977 vtxval 26099 iedgval 26100 vtxvalprc 26158 iedgvalprc 26159 edgval 26162 prcliscplgr 26544 wwlks 26963 wwlksn 26965 clwwlk 27133 clwwlkn 27178 clwwlknOLD 27179 clwwlknonmpt2 27261 vafval 27798 bafval 27799 smfval 27800 vsfval 27828 resvsca 30170 resvlem 30171 mvtval 31735 mexval 31737 mexval2 31738 mdvval 31739 mrsubfval 31743 mrsubrn 31748 mrsub0 31751 mrsubf 31752 mrsubccat 31753 mrsubcn 31754 mrsubco 31756 mrsubvrs 31757 msubfval 31759 elmsubrn 31763 msubrn 31764 msubf 31767 mvhfval 31768 mpstval 31770 msrfval 31772 mstaval 31779 mclsrcl 31796 mppsval 31807 mthmval 31810 sltval2 32146 sltintdifex 32151 fvsingle 32364 funpartfv 32389 fullfunfv 32391 rankeq1o 32615 atbase 35098 llnbase 35317 lplnbase 35342 lvolbase 35386 lhpbase 35806 mzpmfp 37836 kelac1 38159 mendbas 38280 mendplusgfval 38281 mendmulrfval 38283 mendsca 38285 mendvscafval 38286 brfvimex 38850 clsneibex 38926 neicvgbex 38936 upwlkbprop 42247 sprssspr 42259 sprsymrelfvlem 42268 |
Copyright terms: Public domain | W3C validator |