![]() |
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 2566 | . . . . 5 ⊢ (∃!𝑥 𝐴𝐹𝑥 → ∃𝑥 𝐴𝐹𝑥) | |
2 | eldmg 5897 | . . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐹 ↔ ∃𝑥 𝐴𝐹𝑥)) | |
3 | 1, 2 | imbitrrid 245 | . . . 4 ⊢ (𝐴 ∈ V → (∃!𝑥 𝐴𝐹𝑥 → 𝐴 ∈ dom 𝐹)) |
4 | 3 | con3d 152 | . . 3 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → ¬ ∃!𝑥 𝐴𝐹𝑥)) |
5 | tz6.12-2 6881 | . . 3 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅) | |
6 | 4, 5 | syl6 35 | . 2 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅)) |
7 | fvprc 6885 | . . 3 ⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅) | |
8 | 7 | a1d 25 | . 2 ⊢ (¬ 𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅)) |
9 | 6, 8 | pm2.61i 182 | 1 ⊢ (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1534 ∃wex 1774 ∈ wcel 2099 ∃!weu 2557 Vcvv 3462 ∅c0 4322 class class class wbr 5145 dom cdm 5674 ‘cfv 6546 |
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 5303 ax-pr 5425 |
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 3949 df-un 3951 df-ss 3963 df-nul 4323 df-if 4524 df-sn 4624 df-pr 4626 df-op 4630 df-uni 4906 df-br 5146 df-dm 5684 df-iota 6498 df-fv 6554 |
This theorem is referenced by: ndmfvrcl 6929 elfvdm 6930 nfvres 6934 fvfundmfvn0 6936 0fv 6937 funfv 6981 fvun1 6985 fvco4i 6995 fvmpti 7000 mptrcl 7010 fvmptss 7013 fvmptex 7015 fvmptnf 7023 fvmptss2 7027 elfvmptrab1 7029 fvopab4ndm 7031 f0cli 7104 funiunfv 7255 funeldmb 7363 ovprc 7454 oprssdm 7599 nssdmovg 7600 ndmovg 7601 1st2val 8023 2nd2val 8024 brovpreldm 8095 soseq 8165 smofvon2 8378 rdgsucmptnf 8451 frsucmptn 8461 brwitnlem 8529 undifixp 8955 r1tr 9812 rankvaln 9835 cardidm 9995 carden2a 10002 carden2b 10003 carddomi2 10006 sdomsdomcardi 10007 pm54.43lem 10036 alephcard 10106 alephnbtwn 10107 alephgeom 10118 cfub 10283 cardcf 10286 cflecard 10287 cfle 10288 cflim2 10297 cfidm 10309 itunisuc 10453 itunitc1 10454 ituniiun 10456 alephadd 10611 alephreg 10616 pwcfsdom 10617 cfpwsdom 10618 adderpq 10990 mulerpq 10991 uzssz 12889 ltweuz 13975 wrdsymb0 14552 lsw0 14568 swrd00 14647 swrd0 14661 pfx00 14677 pfx0 14678 sumz 15721 sumss 15723 sumnul 15759 prod1 15941 prodss 15944 divsfval 17557 cidpropd 17718 lubval 18376 glbval 18389 joinval 18397 meetval 18411 gsumpropd2lem 18667 mulgfval 19059 mpfrcl 22096 iscnp2 23231 setsmstopn 24474 tngtopn 24655 dvbsss 25919 perfdvf 25920 dchrrcl 27266 nofv 27684 sltres 27689 noseponlem 27691 noextenddif 27695 noextendlt 27696 noextendgt 27697 nolesgn2ores 27699 nogesgn1ores 27701 fvnobday 27705 nosepdmlem 27710 nosepssdm 27713 nosupbnd1lem3 27737 nosupbnd1lem5 27739 nosupbnd2lem1 27742 noinfbnd1lem3 27752 noinfbnd1lem5 27754 noinfbnd2lem1 27757 newval 27876 leftval 27884 rightval 27885 lltropt 27893 madess 27897 oldssmade 27898 lrold 27917 structiedg0val 28955 snstriedgval 28971 rgrx0nd 29528 vsfval 30563 dmadjrnb 31836 hmdmadj 31870 rdgprc0 35630 fullfunfv 35784 linedegen 35980 bj-inftyexpitaudisj 36925 bj-inftyexpidisj 36930 bj-fvimacnv0 37006 dibvalrel 40875 dicvalrelN 40897 dihvalrel 40991 itgocn 42862 fpwfvss 43116 r1rankcld 43942 grur1cld 43943 uz0 45063 climfveq 45326 climfveqf 45337 afv2ndeffv0 46909 fvmptrabdm 46942 fvconstr 48259 fvconstrn0 48260 fvconstr2 48261 fvconst0ci 48262 fvconstdomi 48263 ipolub00 48355 |
Copyright terms: Public domain | W3C validator |