![]() |
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 2596 | . . . . 5 ⊢ (∃!𝑥 𝐴𝐹𝑥 → ∃𝑥 𝐴𝐹𝑥) | |
2 | eldmg 5564 | . . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐹 ↔ ∃𝑥 𝐴𝐹𝑥)) | |
3 | 1, 2 | syl5ibr 238 | . . . 4 ⊢ (𝐴 ∈ V → (∃!𝑥 𝐴𝐹𝑥 → 𝐴 ∈ dom 𝐹)) |
4 | 3 | con3d 150 | . . 3 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → ¬ ∃!𝑥 𝐴𝐹𝑥)) |
5 | tz6.12-2 6436 | . . 3 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅) | |
6 | 4, 5 | syl6 35 | . 2 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅)) |
7 | fvprc 6439 | . . 3 ⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅) | |
8 | 7 | a1d 25 | . 2 ⊢ (¬ 𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅)) |
9 | 6, 8 | pm2.61i 177 | 1 ⊢ (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1601 ∃wex 1823 ∈ wcel 2106 ∃!weu 2585 Vcvv 3397 ∅c0 4140 class class class wbr 4886 dom cdm 5355 ‘cfv 6135 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2054 ax-8 2108 ax-9 2115 ax-10 2134 ax-11 2149 ax-12 2162 ax-13 2333 ax-ext 2753 ax-nul 5025 ax-pow 5077 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2550 df-eu 2586 df-clab 2763 df-cleq 2769 df-clel 2773 df-nfc 2920 df-ral 3094 df-rex 3095 df-rab 3098 df-v 3399 df-dif 3794 df-un 3796 df-in 3798 df-ss 3805 df-nul 4141 df-if 4307 df-sn 4398 df-pr 4400 df-op 4404 df-uni 4672 df-br 4887 df-dm 5365 df-iota 6099 df-fv 6143 |
This theorem is referenced by: ndmfvrcl 6477 elfvdm 6478 elfvdmOLD 6479 nfvres 6483 fvfundmfvn0 6485 0fv 6486 funfv 6525 fvun1 6529 fvco4i 6536 fvmpti 6541 mptrcl 6550 fvmptss 6553 fvmptex 6555 fvmptnf 6563 fvmptss2 6566 elfvmptrab1 6567 fvopab4ndm 6569 f0cli 6634 funiunfv 6778 ovprc 6959 oprssdm 7092 nssdmovg 7093 ndmovg 7094 1st2val 7473 2nd2val 7474 brovpreldm 7535 smofvon2 7736 rdgsucmptnf 7808 frsucmptn 7817 brwitnlem 7871 undifixp 8230 r1tr 8936 rankvaln 8959 cardidm 9118 carden2a 9125 carden2b 9126 carddomi2 9129 sdomsdomcardi 9130 pm54.43lem 9158 alephcard 9226 alephnbtwn 9227 alephgeom 9238 cfub 9406 cardcf 9409 cflecard 9410 cfle 9411 cflim2 9420 cfidm 9432 itunisuc 9576 itunitc1 9577 ituniiun 9579 alephadd 9734 alephreg 9739 pwcfsdom 9740 cfpwsdom 9741 adderpq 10113 mulerpq 10114 uzssz 12012 ltweuz 13079 wrdsymb0 13639 lsw0 13655 swrd00 13734 swrd0 13753 pfx00 13783 pfx0 13784 sumz 14860 sumss 14862 sumnul 14896 prod1 15077 prodss 15080 divsfval 16593 cidpropd 16755 arwval 17078 coafval 17099 lubval 17370 glbval 17383 joinval 17391 meetval 17405 gsumpropd2lem 17659 mpfrcl 19914 iscnp2 21451 setsmstopn 22691 tngtopn 22862 pcofval 23217 dvbsss 24103 perfdvf 24104 dchrrcl 25417 eleenn 26245 structiedg0val 26370 snstriedgval 26386 rgrx0nd 26942 vsfval 28060 dmadjrnb 29337 hmdmadj 29371 funeldmb 32254 rdgprc0 32287 soseq 32343 nofv 32399 sltres 32404 noseponlem 32406 noextenddif 32410 noextendlt 32411 noextendgt 32412 nolesgn2ores 32414 fvnobday 32418 nosepdmlem 32422 nosepssdm 32425 nosupbnd1lem3 32445 nosupbnd1lem5 32447 nosupbnd2lem1 32450 fullfunfv 32643 linedegen 32839 bj-inftyexpitaudisj 33682 bj-inftyexpidisj 33687 dibvalrel 37301 dicvalrelN 37323 dihvalrel 37417 itgocn 38675 uz0 40527 climfveq 40791 climfveqf 40802 afv2ndeffv0 42283 fvmptrabdm 42316 setrec2lem1 43527 |
Copyright terms: Public domain | W3C validator |