Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ndmfv | Structured version Visualization version GIF version |
Description: The value of a class outside its domain is the empty set. (An artifact of our function value definition.) (Contributed by NM, 24-Aug-1995.) |
Ref | Expression |
---|---|
ndmfv | ⊢ (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | euex 2658 | . . . . 5 ⊢ (∃!𝑥 𝐴𝐹𝑥 → ∃𝑥 𝐴𝐹𝑥) | |
2 | eldmg 5761 | . . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐹 ↔ ∃𝑥 𝐴𝐹𝑥)) | |
3 | 1, 2 | syl5ibr 247 | . . . 4 ⊢ (𝐴 ∈ V → (∃!𝑥 𝐴𝐹𝑥 → 𝐴 ∈ dom 𝐹)) |
4 | 3 | con3d 155 | . . 3 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → ¬ ∃!𝑥 𝐴𝐹𝑥)) |
5 | tz6.12-2 6654 | . . 3 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅) | |
6 | 4, 5 | syl6 35 | . 2 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅)) |
7 | fvprc 6657 | . . 3 ⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅) | |
8 | 7 | a1d 25 | . 2 ⊢ (¬ 𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅)) |
9 | 6, 8 | pm2.61i 183 | 1 ⊢ (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1528 ∃wex 1771 ∈ wcel 2105 ∃!weu 2649 Vcvv 3495 ∅c0 4290 class class class wbr 5058 dom cdm 5549 ‘cfv 6349 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 ax-nul 5202 ax-pow 5258 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3497 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4466 df-sn 4560 df-pr 4562 df-op 4566 df-uni 4833 df-br 5059 df-dm 5559 df-iota 6308 df-fv 6357 |
This theorem is referenced by: ndmfvrcl 6695 elfvdm 6696 nfvres 6700 fvfundmfvn0 6702 0fv 6703 funfv 6744 fvun1 6748 fvco4i 6756 fvmpti 6761 mptrcl 6770 fvmptss 6773 fvmptex 6775 fvmptnf 6783 fvmptss2 6786 elfvmptrab1 6788 fvopab4ndm 6790 f0cli 6857 funiunfv 6998 ovprc 7183 oprssdm 7318 nssdmovg 7319 ndmovg 7320 1st2val 7708 2nd2val 7709 brovpreldm 7775 smofvon2 7984 rdgsucmptnf 8056 frsucmptn 8065 brwitnlem 8123 undifixp 8487 r1tr 9194 rankvaln 9217 cardidm 9377 carden2a 9384 carden2b 9385 carddomi2 9388 sdomsdomcardi 9389 pm54.43lem 9417 alephcard 9485 alephnbtwn 9486 alephgeom 9497 cfub 9660 cardcf 9663 cflecard 9664 cfle 9665 cflim2 9674 cfidm 9686 itunisuc 9830 itunitc1 9831 ituniiun 9833 alephadd 9988 alephreg 9993 pwcfsdom 9994 cfpwsdom 9995 adderpq 10367 mulerpq 10368 uzssz 12253 ltweuz 13319 wrdsymb0 13891 lsw0 13907 swrd00 13996 swrd0 14010 pfx00 14026 pfx0 14027 sumz 15069 sumss 15071 sumnul 15105 prod1 15288 prodss 15291 divsfval 16810 cidpropd 16970 lubval 17584 glbval 17597 joinval 17605 meetval 17619 gsumpropd2lem 17879 mulgfval 18166 mpfrcl 20228 iscnp2 21777 setsmstopn 23017 tngtopn 23188 dvbsss 24429 perfdvf 24430 dchrrcl 25744 structiedg0val 26735 snstriedgval 26751 rgrx0nd 27304 vsfval 28338 dmadjrnb 29611 hmdmadj 29645 funeldmb 32904 rdgprc0 32936 soseq 32994 nofv 33062 sltres 33067 noseponlem 33069 noextenddif 33073 noextendlt 33074 noextendgt 33075 nolesgn2ores 33077 fvnobday 33081 nosepdmlem 33085 nosepssdm 33088 nosupbnd1lem3 33108 nosupbnd1lem5 33110 nosupbnd2lem1 33113 fullfunfv 33306 linedegen 33502 bj-inftyexpitaudisj 34380 bj-inftyexpidisj 34385 bj-fvimacnv0 34457 dibvalrel 38181 dicvalrelN 38203 dihvalrel 38297 itgocn 39644 r1rankcld 40447 grur1cld 40448 uz0 41566 climfveq 41830 climfveqf 41841 afv2ndeffv0 43340 fvmptrabdm 43373 setrec2lem1 44694 |
Copyright terms: Public domain | W3C validator |