| 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 6899 for a proof that uses ax-pow 5365 instead of ax-pr 5432. (Contributed by NM, 20-May-1998.) Avoid ax-pow 5365. (Revised by BTernaryTau, 3-Aug-2024.) (Proof shortened by BTernaryTau, 3-Dec-2024.) |
| Ref | Expression |
|---|---|
| fvprc | ⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | brprcneu 6896 | . 2 ⊢ (¬ 𝐴 ∈ V → ¬ ∃!𝑥 𝐴𝐹𝑥) | |
| 2 | tz6.12-2 6894 | . 2 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 = wceq 1540 ∈ wcel 2108 ∃!weu 2568 Vcvv 3480 ∅c0 4333 class class class wbr 5143 ‘cfv 6561 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-nul 5306 ax-pr 5432 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-iota 6514 df-fv 6569 |
| This theorem is referenced by: rnfvprc 6900 dffv3 6902 fvrn0 6936 ndmfv 6941 fv2prc 6951 csbfv 6956 dffv2 7004 brfvopabrbr 7013 fvmpti 7015 fvmptnf 7038 fvmptrabfv 7048 fvunsn 7199 fvmptopab 7487 fvmptopabOLD 7488 brfvopab 7490 1stval 8016 2ndval 8017 fipwuni 9466 fipwss 9469 tctr 9780 ranklim 9884 rankuni 9903 alephsing 10316 itunisuc 10459 itunitc 10461 tskmcl 10881 hashfn 14414 s1prc 14642 trclfvg 15054 trclfvcotrg 15055 dfrtrclrec2 15097 rtrclreclem4 15100 dfrtrcl2 15101 strfvss 17224 strfvi 17227 fveqprc 17228 oveqprc 17229 setsnidOLD 17246 elbasfv 17253 ressbas 17280 ressbasOLD 17281 resslemOLD 17288 firest 17477 topnval 17479 homffval 17733 comfffval 17741 oppchomfval 17757 xpcbas 18223 oduval 18333 oduleval 18334 lubfun 18397 glbfun 18410 odujoin 18453 odumeet 18455 oduclatb 18552 ipopos 18581 isipodrs 18582 plusffval 18659 grpidval 18674 gsum0 18697 ismnd 18750 frmdplusg 18867 frmd0 18873 efmndbas 18884 efmndbasabf 18885 efmndplusg 18893 dfgrp2e 18981 grpinvfval 18996 grpinvfvalALT 18997 grpinvfvi 19000 grpsubfval 19001 grpsubfvalALT 19002 mulgfval 19087 mulgfvalALT 19088 mulgfvi 19091 cntrval 19337 cntzval 19339 cntzrcl 19345 oppgval 19365 oppgplusfval 19366 symgval 19388 lactghmga 19423 psgnfval 19518 odfval 19550 odfvalALT 19551 oppglsm 19660 efgval 19735 mgpval 20140 mgpplusg 20141 ringidval 20180 opprval 20335 opprmulfval 20336 dvdsrval 20361 invrfval 20389 dvrfval 20402 rrgval 20697 staffval 20842 scaffval 20878 islss 20932 sralem 21175 sralemOLD 21176 sravsca 21185 sravscaOLD 21186 sraip 21187 rlmval 21198 rlmsca2 21206 2idlval 21261 zrhval 21518 zlmlemOLD 21528 zlmvsca 21536 chrval 21538 evpmss 21604 ipffval 21666 ocvval 21685 elocv 21686 thlbas 21714 thlbasOLD 21715 thlle 21716 thlleOLD 21717 thloc 21719 pjfval 21726 asclfval 21899 psrbas 21953 psr1val 22187 vr1val 22193 ply1val 22195 ply1basfvi 22242 ply1plusgfvi 22243 psr1sca2 22252 ply1sca2 22255 ply1ascl 22261 evl1fval 22332 evl1fval1 22335 toponsspwpw 22928 istps 22940 tgdif0 22999 indislem 23007 txindislem 23641 fsubbas 23875 filuni 23893 ussval 24268 isusp 24270 nmfval 24601 tnglemOLD 24654 tngds 24668 tngdsOLD 24669 tcphval 25252 deg1fval 26119 deg1fvi 26124 uc1pval 26179 mon1pval 26181 sltval2 27701 sltintdifex 27706 ttglemOLD 28886 vtxval 29017 iedgval 29018 vtxvalprc 29062 iedgvalprc 29063 edgval 29066 prcliscplgr 29431 wwlks 29855 wwlksn 29857 clwwlk 30002 clwwlkn 30045 clwwlknonmpo 30108 vafval 30622 bafval 30623 smfval 30624 vsfval 30652 erlval 33262 fracval 33306 fracbas 33307 resvsca 33356 resvlemOLD 33358 prclisacycgr 35156 mvtval 35505 mexval 35507 mexval2 35508 mdvval 35509 mrsubfval 35513 msubfval 35529 elmsubrn 35533 mvhfval 35538 mpstval 35540 msrfval 35542 mstaval 35549 mclsrcl 35566 mppsval 35577 mthmval 35580 fvsingle 35921 funpartfv 35946 fullfunfv 35948 rankeq1o 36172 atbase 39290 llnbase 39511 lplnbase 39536 lvolbase 39580 lhpbase 40000 mzpmfp 42758 kelac1 43075 mendbas 43192 mendplusgfval 43193 mendmulrfval 43195 mendvscafval 43198 brfvimex 44039 clsneibex 44115 neicvgbex 44125 sprssspr 47468 sprsymrelfvlem 47477 prprelprb 47504 prprspr2 47505 upwlkbprop 48054 ipolub00 48882 |
| Copyright terms: Public domain | W3C validator |