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 5762 | . . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐹 ↔ ∃𝑥 𝐴𝐹𝑥)) | |
3 | 1, 2 | syl5ibr 248 | . . . 4 ⊢ (𝐴 ∈ V → (∃!𝑥 𝐴𝐹𝑥 → 𝐴 ∈ dom 𝐹)) |
4 | 3 | con3d 155 | . . 3 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → ¬ ∃!𝑥 𝐴𝐹𝑥)) |
5 | tz6.12-2 6655 | . . 3 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅) | |
6 | 4, 5 | syl6 35 | . 2 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅)) |
7 | fvprc 6658 | . . 3 ⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅) | |
8 | 7 | a1d 25 | . 2 ⊢ (¬ 𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅)) |
9 | 6, 8 | pm2.61i 184 | 1 ⊢ (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1533 ∃wex 1776 ∈ wcel 2110 ∃!weu 2649 Vcvv 3495 ∅c0 4291 class class class wbr 5059 dom cdm 5550 ‘cfv 6350 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2156 ax-12 2172 ax-ext 2793 ax-nul 5203 ax-pow 5259 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 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 3939 df-un 3941 df-in 3943 df-ss 3952 df-nul 4292 df-if 4468 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4833 df-br 5060 df-dm 5560 df-iota 6309 df-fv 6358 |
This theorem is referenced by: ndmfvrcl 6696 elfvdm 6697 nfvres 6701 fvfundmfvn0 6703 0fv 6704 funfv 6745 fvun1 6749 fvco4i 6757 fvmpti 6762 mptrcl 6772 fvmptss 6775 fvmptex 6777 fvmptnf 6785 fvmptss2 6788 elfvmptrab1 6790 fvopab4ndm 6792 f0cli 6859 funiunfv 7001 ovprc 7188 oprssdm 7323 nssdmovg 7324 ndmovg 7325 1st2val 7711 2nd2val 7712 brovpreldm 7778 smofvon2 7987 rdgsucmptnf 8059 frsucmptn 8068 brwitnlem 8126 undifixp 8492 r1tr 9199 rankvaln 9222 cardidm 9382 carden2a 9389 carden2b 9390 carddomi2 9393 sdomsdomcardi 9394 pm54.43lem 9422 alephcard 9490 alephnbtwn 9491 alephgeom 9502 cfub 9665 cardcf 9668 cflecard 9669 cfle 9670 cflim2 9679 cfidm 9691 itunisuc 9835 itunitc1 9836 ituniiun 9838 alephadd 9993 alephreg 9998 pwcfsdom 9999 cfpwsdom 10000 adderpq 10372 mulerpq 10373 uzssz 12258 ltweuz 13323 wrdsymb0 13895 lsw0 13911 swrd00 14000 swrd0 14014 pfx00 14030 pfx0 14031 sumz 15073 sumss 15075 sumnul 15109 prod1 15292 prodss 15295 divsfval 16814 cidpropd 16974 lubval 17588 glbval 17601 joinval 17609 meetval 17623 gsumpropd2lem 17883 mulgfval 18220 mpfrcl 20292 iscnp2 21841 setsmstopn 23082 tngtopn 23253 dvbsss 24494 perfdvf 24495 dchrrcl 25810 structiedg0val 26801 snstriedgval 26817 rgrx0nd 27370 vsfval 28404 dmadjrnb 29677 hmdmadj 29711 funeldmb 33001 rdgprc0 33033 soseq 33091 nofv 33159 sltres 33164 noseponlem 33166 noextenddif 33170 noextendlt 33171 noextendgt 33172 nolesgn2ores 33174 fvnobday 33178 nosepdmlem 33182 nosepssdm 33185 nosupbnd1lem3 33205 nosupbnd1lem5 33207 nosupbnd2lem1 33210 fullfunfv 33403 linedegen 33599 bj-inftyexpitaudisj 34481 bj-inftyexpidisj 34486 bj-fvimacnv0 34562 dibvalrel 38293 dicvalrelN 38315 dihvalrel 38409 itgocn 39757 r1rankcld 40560 grur1cld 40561 uz0 41678 climfveq 41942 climfveqf 41953 afv2ndeffv0 43452 fvmptrabdm 43485 setrec2lem1 44789 |
Copyright terms: Public domain | W3C validator |